Modifier and Type | Field and Description |
---|---|
private Function |
acc |
private Function |
anon |
private Function |
arr |
static Name |
BASE_HEAP_NAME |
private SortDependingFunction |
classErroneous |
private SortDependingFunction |
classInitializationInProgress |
private SortDependingFunction |
classInitialized |
private SortDependingFunction |
classPrepared |
private Function |
create |
private Function |
created |
private Sort |
fieldSort |
private ImmutableList<LocationVariable> |
heaps |
private Function |
initialized |
private Function |
length |
private Function |
memset |
static Name |
NAME |
private Function |
nullFunc |
static Name |
PERMISSION_HEAP_NAME |
private Function |
prec |
private Function |
reach |
static Name |
SAVED_HEAP_NAME |
private SortDependingFunction |
select |
static Name |
SELECT_NAME |
private Function |
store |
static Name |
STORE_NAME |
static Name[] |
VALID_HEAP_NAMES |
private Function |
wellFormed |
Constructor and Description |
---|
HeapLDT(TermServices services) |
Modifier and Type | Method and Description |
---|---|
boolean |
containsFunction(Function op) |
Function |
getAcc() |
ImmutableList<LocationVariable> |
getAllHeaps() |
Function |
getAnon() |
Function |
getArr() |
Function |
getClassErroneous(Sort instanceSort,
TermServices services) |
Function |
getClassInitializationInProgress(Sort instanceSort,
TermServices services) |
Function |
getClassInitialized(Sort instanceSort,
TermServices services) |
static java.lang.String |
getClassName(Function fieldSymbol)
Extracts the name of the enclosing class from the name of a constant
symbol representing a field.
|
Function |
getClassPrepared(Sort instanceSort,
TermServices services) |
Function |
getCreate() |
Function |
getCreated() |
Sort |
getFieldSort()
Returns the sort "Field".
|
Function |
getFieldSymbolForPV(LocationVariable fieldPV,
Services services)
Given a "program variable" representing a field or a model field,
returns the function symbol representing the same field.
|
private java.lang.String |
getFieldSymbolName(LocationVariable fieldPV) |
Function |
getFunctionFor(Operator op,
Services serv,
ExecutionContext ec)
returns the function symbol for the given operation
|
LocationVariable |
getHeap() |
LocationVariable |
getHeapForName(Name name) |
Function |
getInitialized() |
Function |
getLength() |
Function |
getMemset() |
Function |
getNull() |
LocationVariable |
getPermissionHeap() |
Function |
getPrec() |
static java.lang.String |
getPrettyFieldName(Named fieldSymbol)
Given a constant symbol representing a field, this method returns a
simplified name of the constant symbol to be used for pretty printing.
|
Function |
getReach() |
LocationVariable |
getSavedHeap() |
Function |
getSelect(Sort instanceSort,
TermServices services)
Returns the select function for the given sort.
|
Sort |
getSortOfSelect(Operator op)
If the passed operator is an instance of "select", this method returns
the sort of the function (identical to its return type); otherwise,
returns null.
|
Function |
getStore() |
Type |
getType(Term t) |
Function |
getWellFormed() |
boolean |
hasLiteralFunction(Function f) |
boolean |
isResponsible(Operator op,
Term[] subs,
Services services,
ExecutionContext ec)
returns true if the LDT offers an operation for the given java
operator and the logic subterms
|
boolean |
isResponsible(Operator op,
Term sub,
TermServices services,
ExecutionContext ec)
returns true if the LDT offers an operation for the given
unary java operator and the logic subterms
|
boolean |
isResponsible(Operator op,
Term left,
Term right,
Services services,
ExecutionContext ec)
returns true if the LDT offers an operation for the given
binary java operator and the logic subterms
|
boolean |
isSelectOp(Operator op) |
Term |
translateLiteral(Literal lit,
Services services)
translates a given literal to its logic counterpart
|
Expression |
translateTerm(Term t,
ExtList children,
Services services)
Is called whenever
hasLiteralFunction() returns true. |
addFunction, addFunction, addSortDependingFunction, functions, getNewLDTInstances, name, targetSort, toString
public static final Name NAME
public static final Name SELECT_NAME
public static final Name STORE_NAME
public static final Name BASE_HEAP_NAME
public static final Name SAVED_HEAP_NAME
public static final Name PERMISSION_HEAP_NAME
public static final Name[] VALID_HEAP_NAMES
private final Sort fieldSort
private final SortDependingFunction select
private final Function store
private final Function create
private final Function anon
private final Function memset
private final Function arr
private final Function created
private final Function initialized
private final SortDependingFunction classPrepared
private final SortDependingFunction classInitialized
private final SortDependingFunction classInitializationInProgress
private final SortDependingFunction classErroneous
private final Function length
private final Function nullFunc
private final Function wellFormed
private final Function acc
private final Function reach
private final Function prec
private ImmutableList<LocationVariable> heaps
public HeapLDT(TermServices services)
private java.lang.String getFieldSymbolName(LocationVariable fieldPV)
public static java.lang.String getPrettyFieldName(Named fieldSymbol)
public static java.lang.String getClassName(Function fieldSymbol)
public Sort getFieldSort()
public Function getSelect(Sort instanceSort, TermServices services)
public Sort getSortOfSelect(Operator op)
public boolean isSelectOp(Operator op)
public Function getStore()
public Function getCreate()
public Function getAnon()
public Function getMemset()
public Function getArr()
public Function getCreated()
public Function getInitialized()
public Function getClassPrepared(Sort instanceSort, TermServices services)
public Function getClassInitialized(Sort instanceSort, TermServices services)
public Function getClassInitializationInProgress(Sort instanceSort, TermServices services)
public Function getClassErroneous(Sort instanceSort, TermServices services)
public Function getLength()
public Function getNull()
public Function getWellFormed()
public Function getAcc()
public Function getReach()
public Function getPrec()
public LocationVariable getHeap()
public LocationVariable getSavedHeap()
public ImmutableList<LocationVariable> getAllHeaps()
public LocationVariable getHeapForName(Name name)
public LocationVariable getPermissionHeap()
public Function getFieldSymbolForPV(LocationVariable fieldPV, Services services)
public final boolean containsFunction(Function op)
containsFunction
in class LDT
public boolean isResponsible(Operator op, Term[] subs, Services services, ExecutionContext ec)
LDT
isResponsible
in class LDT
op
- the de.uka.ilkd.key.java.expression.Operator to
translatesubs
- the logic subterms of the java operatorservices
- the Servicesec
- the ExecutionContext in which the expression is evaluatedpublic boolean isResponsible(Operator op, Term left, Term right, Services services, ExecutionContext ec)
LDT
isResponsible
in class LDT
op
- the de.uka.ilkd.key.java.expression.Operator to
translateleft
- the left subterm of the java operatorright
- the right subterm of the java operatorservices
- the Servicesec
- the ExecutionContext in which the expression is evaluatedpublic boolean isResponsible(Operator op, Term sub, TermServices services, ExecutionContext ec)
LDT
isResponsible
in class LDT
op
- the de.uka.ilkd.key.java.expression.Operator to
translatesub
- the logic subterms of the java operatorservices
- the Servicesec
- the ExecutionContext in which the expression is evaluatedpublic Term translateLiteral(Literal lit, Services services)
LDT
translateLiteral
in class LDT
lit
- the Literal to be translatedpublic Function getFunctionFor(Operator op, Services serv, ExecutionContext ec)
LDT
getFunctionFor
in class LDT
public boolean hasLiteralFunction(Function f)
hasLiteralFunction
in class LDT
public Expression translateTerm(Term t, ExtList children, Services services)
LDT
hasLiteralFunction()
returns true.translateTerm
in class LDT