public class MethodCall extends ProgramTransformer
Modifier and Type | Field and Description |
---|---|
protected ImmutableArray<Expression> |
arguments |
private ExecutionContext |
execContext |
private IExecutionContext |
execContextSV |
protected MethodReference |
methRef |
protected ReferencePrefix |
newContext |
private IProgramMethod |
pm |
protected ProgramVariable |
pvar |
private SchemaVariable |
resultVar |
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
|
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
private final SchemaVariable resultVar
protected MethodReference methRef
private IProgramMethod pm
protected ReferencePrefix newContext
protected ProgramVariable pvar
private IExecutionContext execContextSV
private ExecutionContext execContext
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.private ImmutableList<KeYJavaType> getTypes(ImmutableArray<Expression> args, Services services)
private KeYJavaType getStaticPrefixType(ReferencePrefix refPrefix, Services services)
protected IProgramMethod getMethod(KeYJavaType prefixType, MethodReference mr, Services services)
prefixType
- TODOmr
- TODOservices
- TODOprivate IProgramMethod getSuperMethod(ExecutionContext ex, MethodReference mr, Services services)
private KeYJavaType getSuperType(ExecutionContext ex, Services services)
public 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 performedprivate Statement handleInstanceInvocation(Services services, Statement result)
private Statement makeMbs(KeYJavaType t, Services services)
private Expression makeIOf(Type t)
protected Statement makeIfCascade(ImmutableList<KeYJavaType> imps, Services services)
imps
- TODOservices
- The Services object.private VariableSpecification[] createParamSpecs(Services services)
private Expression makeVariableArgument(VariableSpecification originalSpec)
Quote JLS 15.12.4.2 Evaluate Arguments The process of evaluating of the argument list differs, depending on whether the method being invoked is a fixed arity method or a variable arity method (JLS 8.4.1). If the method being invoked is a variable arity method (JLS 8.4.1) m, it necessarily has n>0 formal parameters. The final formal parameter of m necessarily has type T[] for some T, and m is necessarily being invoked with k0 actual argument expressions. If m is being invoked with kn actual argument expressions, or, if m is being invoked with k=n actual argument expressions and the type of the kth argument expression is not assignment compatible with T[], then the argument list (e1, ... , en-1, en, ...ek) is evaluated as if it were written as (e1, ..., en-1, new T[]{en, ..., ek}).Thus, when the last formal parameter is reached and circumstances enforce wrapping arguments in an array, this method creates the expected.
originalSpec
- the original sepcification of the formal paramaterprivate Statement[] createParamAssignments(VariableSpecification[] specs)
private ImmutableArray<Expression> getVariables(VariableSpecification[] varspecs)
private boolean assignmentCompatible(Expression exp, Type type, Services services)
exp
- expression to checktype
- type to check for