public class DLEmbeddedExpression extends Operator
Modifier and Type | Field and Description |
---|---|
private Function |
functionSymbol |
Constructor and Description |
---|
DLEmbeddedExpression(Function f,
ExtList children) |
Modifier and Type | Method and Description |
---|---|
void |
check(Services javaServ,
KeYJavaType containingClass) |
int |
getArity()
Arity of an embedded JavaDL Expression depends upon the number of
arguments.
|
Function |
getFunctionSymbol() |
private static Sort |
getHeapSort(Services javaServ) |
KeYJavaType |
getKeYJavaType(Services javaServ,
ExecutionContext ec)
returns the
KeYJavaType of an expression |
private static KeYJavaType |
getKeYJavaType(Services javaServ,
Sort argSort) |
int |
getNotation() |
int |
getPrecedence()
0 is the "highest" precedence (obtained by parantheses),
13 the "lowest".
|
Term |
makeTerm(LocationVariable heap,
Term[] subs,
Services services) |
void |
prettyPrint(PrettyPrinter p)
Pretty printing the source element.
|
void |
visit(Visitor v)
calls the corresponding method of a visitor in order to
perform some action/transformation on this element
|
getArguments, getChildAt, getChildCount, getExpressionAt, getExpressionCount, getFirstElement, getFirstElementIncludingBlocks, getLastElement, isLeftAssociative, isToBeParenthesized, precedes, reuseSignature
compatibleBlockSize, computeHashCode, equals, equalsModRenaming, getArrayPos, match, matchChildren
getComments, hashCode, prettyPrintMain
getEndPosition, getParentClass, getPositionInfo, getRelativePosition, getStartPosition, setParentClass, toSource, toString, toString
clone, finalize, getClass, notify, notifyAll, wait, wait, wait
getComments, match
equalsModRenaming, getEndPosition, getPositionInfo, getRelativePosition, getStartPosition
private final Function functionSymbol
public Function getFunctionSymbol()
public int getArity()
functionSymbol
.public KeYJavaType getKeYJavaType(Services javaServ, ExecutionContext ec)
Expression
KeYJavaType
of an expressiongetKeYJavaType
in interface Expression
getKeYJavaType
in class Operator
public int getNotation()
getNotation
in class Operator
public int getPrecedence()
Operator
getPrecedence
in class Operator
public void visit(Visitor v)
SourceElement
v
- the Visitorpublic void prettyPrint(PrettyPrinter p) throws java.io.IOException
JavaSourceElement
prettyPrint
in interface SourceElement
prettyPrint
in class JavaProgramElement
p
- a pretty printer.java.io.IOException
- occasionally thrown.public void check(Services javaServ, KeYJavaType containingClass) throws ConvertException
ConvertException
private static KeYJavaType getKeYJavaType(Services javaServ, Sort argSort)
public Term makeTerm(LocationVariable heap, Term[] subs, Services services)