public class Recoder2KeYTypeConverter
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
private CreateArrayMethodBuilder |
arrayMethodBuilder
builder class for implicit array methods
|
private JavaInfo |
javaInfo |
private NamespaceSet |
namespaces
the namespaces to store new types to.
|
private Recoder2KeY |
recoder2key
The associated Recoder<->KeY object
|
private TypeConverter |
typeConverter
The type converter provides methods on key types.
|
Constructor and Description |
---|
Recoder2KeYTypeConverter(Services services,
TypeConverter typeConverter,
NamespaceSet namespaces,
Recoder2KeY recoder2key) |
Modifier and Type | Method and Description |
---|---|
private void |
addImplicitArrayMembers(ExtList members,
KeYJavaType parent,
KeYJavaType baseType,
ProgramVariable len)
Adds several implicit fields and methods to given list of members.
|
private void |
addKeYJavaType(Type t,
Sort s) |
ArrayDeclaration |
createArrayType(KeYJavaType baseType,
KeYJavaType arrayType)
create
|
private Sort |
createObjectSort(ClassType ct,
ImmutableSet<Sort> supers)
create a sort out of a recoder class
|
private FieldDeclaration |
createSuperArrayType()
creates a super type for array types.
|
private ImmutableSet<Sort> |
directSuperSorts(ClassType classType)
get all direct super sorts of a class type (not transitive)
|
private ImmutableList<Field> |
filterField(ExtList list)
extracts all field specifications out of the given list.
|
private ImmutableList<Field> |
filterField(FieldDeclaration field)
extracts all fields out of fielddeclaration
|
KeYJavaType |
getKeYJavaType(java.lang.String typeName)
return the corresponding KeY JavaType for a recoder type.
|
KeYJavaType |
getKeYJavaType(Type t)
return the corresponding KeY JavaType for a recoder type.
|
private Recoder2KeYConverter |
getRecoder2KeYConverter()
get the corresponding Recoder2KeYConverter object of this type converter.
|
private ServiceConfiguration |
getServiceConfiguration() |
TypeConverter |
getTypeConverter() |
private void |
initArrayMethodBuilder() |
private boolean |
isObject(ClassType ct)
is the full name of this type "java.lang.Object" or the short name
"Object"
|
private KeYJavaType |
lookupInCache(Type t) |
private void |
storeInCache(Type t,
KeYJavaType kjt) |
private CreateArrayMethodBuilder arrayMethodBuilder
initArrayMethodBuilder()
private final TypeConverter typeConverter
private final NamespaceSet namespaces
private final Recoder2KeY recoder2key
private JavaInfo javaInfo
public Recoder2KeYTypeConverter(Services services, TypeConverter typeConverter, NamespaceSet namespaces, Recoder2KeY recoder2key)
private KeYJavaType lookupInCache(Type t)
private void storeInCache(Type t, KeYJavaType kjt)
private ServiceConfiguration getServiceConfiguration()
private Recoder2KeYConverter getRecoder2KeYConverter()
public KeYJavaType getKeYJavaType(java.lang.String typeName)
getKeYJavaType(Type)
typeName
- name of a type to be convertedgetKeYJavaType(Type)
public KeYJavaType getKeYJavaType(Type t)
t
- type to be converted, may be nullprivate ImmutableSet<Sort> directSuperSorts(ClassType classType)
classType
- type to examine, not nullprivate boolean isObject(ClassType ct)
ct
- the type to be checked, not nullprivate Sort createObjectSort(ClassType ct, ImmutableSet<Sort> supers)
ct
- classtype to create for, not nullsupers
- the set of (direct?) super-sortspublic ArrayDeclaration createArrayType(KeYJavaType baseType, KeYJavaType arrayType)
baseType
- arrayType
- private FieldDeclaration createSuperArrayType()
length
private void addImplicitArrayMembers(ExtList members, KeYJavaType parent, KeYJavaType baseType, ProgramVariable len)
members
- an ExtList with the members of parentparent
- the KeYJavaType of the array to be enriched by its implicit
membersbaseType
- the KeYJavaType of the parent's element typeprivate ImmutableList<Field> filterField(FieldDeclaration field)
field
- the FieldDeclaration of which the field specifications have to
be extractedprivate ImmutableList<Field> filterField(ExtList list)
list
- the ExtList with the members of a type declarationprivate void initArrayMethodBuilder()
public TypeConverter getTypeConverter()