public final class TypeConverter
extends java.lang.Object
public void init()
public ImmutableList<LDT> getModels()
public IntegerLDT getIntegerLDT()
public BooleanLDT getBooleanLDT()
public LocSetLDT getLocSetLDT()
public HeapLDT getHeapLDT()
public PermissionLDT getPermissionLDT()
public SeqLDT getSeqLDT()
public MapLDT getMapLDT()
public CharListLDT getCharListLDT()
public Term findThisForSortExact(Sort s, ExecutionContext ec)
public Term findThisForSort(Sort s, ExecutionContext ec)
public Term findThisForSort(Sort s, Term self, KeYJavaType context, boolean exact)
public Term convertMethodReference(MethodReference mr, ExecutionContext ec)
public Term convertVariableReference(VariableReference fr, ExecutionContext ec)
public Term convertArrayReference(ArrayReference ar, ExecutionContext ec)
public Term convertToLogicElement(ProgramElement pe)
public Term convertToLogicElement(ProgramElement pe, ExecutionContext ec)
public static boolean isArithmeticOperator(Operator op)
public KeYJavaType getPromotedType(KeYJavaType type1, KeYJavaType type2)
public boolean isIntegerType(Type t2)
public KeYJavaType getPromotedType(KeYJavaType type1)
public KeYJavaType getBooleanType()
public KeYJavaType getKeYJavaType(Expression e)
For these cases please use @link #getKeYJavaType(Expression, ExecutionContext)
This method behaves same as invoking getKeYJavaType(e, null)
public KeYJavaType getKeYJavaType(Expression e, ExecutionContext ec)
e
- the Expression whose type has to be retrievedec
- the ExecutionContext of expression epublic Expression convertToProgramElement(Term term)
term
- the Term to be convertedjava.lang.RuntimeException
- iff a conversion is not possiblepublic KeYJavaType getKeYJavaType(Term t)
public KeYJavaType getKeYJavaType(Type t)
public boolean isWidening(PrimitiveType from, PrimitiveType to)
public boolean isWidening(KeYJavaType from, KeYJavaType to)
public boolean isImplicitNarrowing(Expression expr, PrimitiveType to)
public boolean isAssignableTo(Expression expr, Type to, ExecutionContext ec)
public boolean isNarrowing(KeYJavaType from, KeYJavaType to)
public boolean isNarrowing(PrimitiveType from, PrimitiveType to)
public boolean isNumericalType(Type t)
public boolean isIntegralType(Type t)
public boolean isReferenceType(Type t)
public boolean isNullType(Type t)
public boolean isBooleanType(Type t)
public TypeConverter copy(Services services)
Copyright © 2003-2019 The KeY-Project.