de.uka.ilkd.key.rule.metaconstruct

Class EvaluateArgs

java.lang.Object

de.uka.ilkd.key.java.JavaSourceElement

de.uka.ilkd.key.java.JavaProgramElement

de.uka.ilkd.key.java.JavaNonTerminalProgramElement

de.uka.ilkd.key.rule.metaconstruct.ProgramTransformer

de.uka.ilkd.key.rule.metaconstruct.EvaluateArgs

All Implemented Interfaces:

Expression, ExpressionContainer, ModelElement, NamedModelElement, NamedProgramElement, NonTerminalProgramElement, ProgramElement, Reference, MemberReference, NameReference, PackageReferenceContainer, ReferencePrefix, ReferenceSuffix, TypeReference, TypeReferenceContainer, TypeReferenceInfix, SourceElement, Statement, StatementContainer, SVSubstitute

public class EvaluateArgs
extends ProgramTransformer

TODO

Author:

N/A

Constructor Summary

Constructors

Constructor and Description
EvaluateArgs(ProgramElement pe) creates a typeof ProgramTransformer

Method Summary

Modifier and Type	Method and Description
static ProgramVariable	evaluate(Expression e, java.util.List<? super LocalVariableDeclaration> l, Services services, ExecutionContext ec) TODO Comment.
ProgramElement[]	transform(ProgramElement pe, Services services, SVInstantiations svInst) performs the program transformation needed for symbolic program transformation

Methods inherited from class de.uka.ilkd.key.rule.metaconstruct.ProgramTransformer

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

Methods inherited from class de.uka.ilkd.key.java.JavaNonTerminalProgramElement

compatibleBlockSize, computeHashCode, equals, equalsModRenaming, getArrayPos, match, matchChildren

Methods inherited from class de.uka.ilkd.key.java.JavaProgramElement

getComments, hashCode, prettyPrintMain, reuseSignature

Methods inherited from class de.uka.ilkd.key.java.JavaSourceElement

getEndPosition, getFirstElement, getFirstElementIncludingBlocks, getParentClass, getPositionInfo, getRelativePosition, getStartPosition, setParentClass, toSource, toString

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Methods inherited from interface de.uka.ilkd.key.java.ProgramElement

getComments, match

Constructor Detail

EvaluateArgs

public EvaluateArgs(ProgramElement pe)

creates a typeof ProgramTransformer

Parameters:

pe - the instance of expression contained by the meta construct

Method Detail

evaluate

public static ProgramVariable evaluate(Expression e,
                                       java.util.List<? super LocalVariableDeclaration> l,
                                       Services services,
                                       ExecutionContext ec)

TODO Comment.

Parameters:

e - TODO

l - TODO

services - TODO

ec - TODO

Returns:

TODO

transform

public ProgramElement[] transform(ProgramElement pe,
                                  Services services,
                                  SVInstantiations svInst)

Description copied from class: ProgramTransformer

performs the program transformation needed for symbolic program transformation

Specified by:

transform in class ProgramTransformer

Parameters:

pe - the ProgramElement on which the execution is performed

services - the Services with all necessary information about the java programs

svInst - the instantiations of the schemavariables

Returns:

the transformated program