All Methods Static Methods Instance Methods Concrete Methods
Modifier and Type |
Method and Description |
Term |
convertArrayReference(ArrayReference ar,
ExecutionContext ec) |
private Term |
convertLiteralExpression(Literal lit)
dispatches the given literal and converts it
|
Term |
convertMethodReference(MethodReference mr,
ExecutionContext ec) |
private Term |
convertReferencePrefix(ReferencePrefix prefix,
ExecutionContext ec) |
private Term |
convertToInstanceofTerm(Instanceof io,
ExecutionContext ec) |
Term |
convertToLogicElement(ProgramElement pe) |
Term |
convertToLogicElement(ProgramElement pe,
ExecutionContext ec) |
Expression |
convertToProgramElement(Term term)
converts a logical term to an AST node if possible.
|
Term |
convertVariableReference(VariableReference fr,
ExecutionContext ec) |
TypeConverter |
copy(Services services) |
Term |
findThisForSort(Sort s,
ExecutionContext ec) |
Term |
findThisForSort(Sort s,
Term self,
KeYJavaType context,
boolean exact) |
Term |
findThisForSortExact(Sort s,
ExecutionContext ec) |
BooleanLDT |
getBooleanLDT() |
KeYJavaType |
getBooleanType() |
CharListLDT |
getCharListLDT() |
HeapLDT |
getHeapLDT() |
IntegerLDT |
getIntegerLDT() |
KeYJavaType |
getKeYJavaType(Expression e)
Retrieves the static type of the expression.
|
KeYJavaType |
getKeYJavaType(Expression e,
ExecutionContext ec)
retrieves the type of the expression e with respect to
the context in which it is evaluated
|
KeYJavaType |
getKeYJavaType(Term t) |
KeYJavaType |
getKeYJavaType(Type t) |
private LDT |
getLDT(Name ldtName) |
LocSetLDT |
getLocSetLDT() |
MapLDT |
getMapLDT() |
LDT |
getModelFor(Sort s) |
ImmutableList<LDT> |
getModels() |
PermissionLDT |
getPermissionLDT() |
Sort |
getPrimitiveSort(Type t) |
KeYJavaType |
getPromotedType(KeYJavaType type1) |
KeYJavaType |
getPromotedType(KeYJavaType type1,
KeYJavaType type2)
performs binary numeric promotion on the argument types
|
private LDT |
getResponsibleLDT(Operator op,
Term[] subs,
Services services,
ExecutionContext ec) |
SeqLDT |
getSeqLDT() |
void |
init() |
private void |
init(java.util.Map<Name,LDT> map) |
static boolean |
isArithmeticOperator(Operator op) |
boolean |
isAssignableTo(Expression expr,
Type to,
ExecutionContext ec) |
boolean |
isAssignableTo(Type from,
Type to) |
boolean |
isBooleanType(Type t) |
boolean |
isCastingTo(Type from,
Type to) |
boolean |
isIdentical(Type from,
Type to) |
boolean |
isImplicitNarrowing(Expression expr,
PrimitiveType to) |
boolean |
isIntegerType(Type t2) |
boolean |
isIntegralType(Type t) |
boolean |
isNarrowing(ArrayType from,
ArrayType to) |
boolean |
isNarrowing(ClassType from,
ClassType to) |
boolean |
isNarrowing(KeYJavaType from,
KeYJavaType to) |
boolean |
isNarrowing(PrimitiveType from,
PrimitiveType to) |
boolean |
isNarrowing(Type from,
Type to) |
boolean |
isNullType(Type t) |
boolean |
isNumericalType(Type t) |
boolean |
isReferenceType(Type t) |
boolean |
isWidening(ArrayType from,
ArrayType to) |
boolean |
isWidening(ClassType from,
ClassType to) |
boolean |
isWidening(KeYJavaType from,
KeYJavaType to) |
boolean |
isWidening(PrimitiveType from,
PrimitiveType to)
These methods are taken from recoder (and modified)
|
boolean |
isWidening(Type from,
Type to) |
private Expression |
translateJavaCast(Term term,
ExtList children) |
private Term |
translateOperator(Operator op,
ExecutionContext ec) |