public class MethodCall extends ProgramTransformer
Modifier and Type | Field and Description |
---|---|
protected ImmutableArray<Expression> |
arguments |
protected MethodReference |
methRef |
protected ReferencePrefix |
newContext |
protected ProgramVariable |
pvar |
protected KeYJavaType |
staticPrefixType |
Modifier | Constructor and Description |
---|---|
protected |
MethodCall(Name name,
ProgramSV ec,
SchemaVariable result,
ProgramElement body)
creates the methodcall-MetaConstruct
|
|
MethodCall(ProgramElement body)
creates the methodcall-MetaConstruct
|
|
MethodCall(ProgramSV ec,
SchemaVariable result,
ProgramElement body)
creates the methodcall-MetaConstruct
|
|
MethodCall(SchemaVariable result,
ProgramElement body)
creates the methodcall-MetaConstruct
|
Modifier and Type | Method and Description |
---|---|
protected IProgramMethod |
getMethod(KeYJavaType prefixType,
MethodReference mr,
Services services)
Returns the method.
|
protected Statement |
makeIfCascade(ImmutableList<KeYJavaType> imps,
Services services)
TODO
|
ProgramElement[] |
transform(ProgramElement pe,
Services services,
SVInstantiations svInst)
performs the program transformation needed for symbolic program execution
|
body, getChildAt, getChildCount, getDimensions, getExpressionAt, getExpressionCount, getKeYJavaType, getKeYJavaType, getKeYJavaType, getLastElement, getName, getPackageReference, getProgramElementName, getReferencePrefix, getStatementAt, getStatementCount, getTypeReferenceAt, getTypeReferenceCount, name, neededInstantiations, needs, prettyPrint, setReferencePrefix, toString, visit
compatibleBlockSize, computeHashCode, equals, equalsModRenaming, getArrayPos, match, matchChildren
getComments, hashCode, prettyPrintMain, reuseSignature
getEndPosition, getFirstElement, getFirstElementIncludingBlocks, getParentClass, getPositionInfo, getRelativePosition, getStartPosition, setParentClass, toSource, toString
clone, finalize, getClass, notify, notifyAll, wait, wait, wait
getComments, match
protected MethodReference methRef
protected ReferencePrefix newContext
protected ProgramVariable pvar
protected ImmutableArray<Expression> arguments
protected KeYJavaType staticPrefixType
public MethodCall(ProgramElement body)
body
- the ProgramElement contained by the meta constructpublic MethodCall(SchemaVariable result, ProgramElement body)
result
- the SchemaVariable that is used to keep the resultbody
- the ProgramElement contained by the meta constructpublic MethodCall(ProgramSV ec, SchemaVariable result, ProgramElement body)
result
- the SchemaVariable that is used to keep the resultbody
- the ProgramElement contained by the meta constructprotected MethodCall(Name name, ProgramSV ec, SchemaVariable result, ProgramElement body)
result
- the SchemaVariable that is used to keep the resultbody
- the ProgramElement contained by the meta constructname
- Method name.ec
- The Schema Variable.protected IProgramMethod getMethod(KeYJavaType prefixType, MethodReference mr, Services services)
prefixType
- TODOmr
- TODOservices
- TODOpublic ProgramElement[] transform(ProgramElement pe, Services services, SVInstantiations svInst)
transform
in class ProgramTransformer
services
- the Services with all necessary information about the java
programssvInst
- the instantiations esp. of the inner and outer labelpe
- the ProgramElement on which the execution is performedprotected Statement makeIfCascade(ImmutableList<KeYJavaType> imps, Services services)
imps
- TODOservices
- The Services object.Copyright © 2003-2019 The KeY-Project.