de.uka.ilkd.key.java.expression.operator

Class DLEmbeddedExpression

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.java.expression.Operator

de.uka.ilkd.key.java.expression.operator.DLEmbeddedExpression

All Implemented Interfaces:

Expression, ExpressionContainer, ModelElement, NonTerminalProgramElement, ProgramElement, SourceElement, SVSubstitute

public class DLEmbeddedExpression
extends Operator

Field Summary

Fields

Modifier and Type	Field and Description
private Function	functionSymbol

Fields inherited from class de.uka.ilkd.key.java.expression.Operator

children, INFIX, POSTFIX, PREFIX

Constructor Summary

Constructors

Constructor and Description
DLEmbeddedExpression(Function f, ExtList children)

Method Summary

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

Methods inherited from class de.uka.ilkd.key.java.expression.Operator

getArguments, getChildAt, getChildCount, getExpressionAt, getExpressionCount, getFirstElement, getFirstElementIncludingBlocks, getLastElement, isLeftAssociative, isToBeParenthesized, precedes, reuseSignature

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

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

getEndPosition, getParentClass, getPositionInfo, getRelativePosition, getStartPosition, setParentClass, toSource, toString, 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

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

equalsModRenaming, getEndPosition, getPositionInfo, getRelativePosition, getStartPosition

Field Detail

functionSymbol

private final Function functionSymbol

Constructor Detail

DLEmbeddedExpression

public DLEmbeddedExpression(Function f,
                            ExtList children)

Method Detail

getFunctionSymbol

public Function getFunctionSymbol()

Returns:

the functionSymbol

getArity

public int getArity()

Arity of an embedded JavaDL Expression depends upon the number of arguments. Since the first argument may be implicitly given, we cannot use the arity of functionSymbol.

Specified by:

getArity in class Operator

getKeYJavaType

public KeYJavaType getKeYJavaType(Services javaServ,
                                  ExecutionContext ec)

Description copied from interface: Expression

returns the KeYJavaType of an expression

Specified by:

getKeYJavaType in interface Expression

Specified by:

getKeYJavaType in class Operator

getNotation

public int getNotation()

Specified by:

getNotation in class Operator

Returns:

INFIX, PREFIX, or POSTFIX.

getPrecedence

public int getPrecedence()

Description copied from class: Operator

0 is the "highest" precedence (obtained by parantheses), 13 the "lowest".

Specified by:

getPrecedence in class Operator

visit

public void visit(Visitor v)

Description copied from interface: SourceElement

calls the corresponding method of a visitor in order to perform some action/transformation on this element

Parameters:

v - the Visitor

prettyPrint

public void prettyPrint(PrettyPrinter p)
                 throws java.io.IOException

Description copied from class: JavaSourceElement

Pretty printing the source element.

Specified by:

prettyPrint in interface SourceElement

Overrides:

prettyPrint in class JavaProgramElement

Parameters:

p - a pretty printer.

Throws:

java.io.IOException - occasionally thrown.

check

public void check(Services javaServ,
                  KeYJavaType containingClass)
           throws ConvertException

Throws:

ConvertException

getHeapSort

private static Sort getHeapSort(Services javaServ)

getKeYJavaType

private static KeYJavaType getKeYJavaType(Services javaServ,
                                          Sort argSort)

makeTerm

public Term makeTerm(LocationVariable heap,
                     Term[] subs,
                     Services services)