public class KeYProgModelInfo
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
private KeYRecoderExcHandler |
exceptionHandler |
private java.util.HashMap<KeYJavaType,java.util.HashMap<java.lang.String,IProgramMethod>> |
implicits |
private KeYRecoderMapping |
mapping |
private KeYCrossReferenceServiceConfiguration |
sc |
private Services |
services |
private TypeConverter |
typeConverter |
Constructor and Description |
---|
KeYProgModelInfo(Services services,
KeYCrossReferenceServiceConfiguration crsc,
KeYRecoderMapping krm,
TypeConverter typeConverter) |
KeYProgModelInfo(Services services,
TypeConverter typeConverter,
KeYRecoderExcHandler keh) |
Modifier and Type | Method and Description |
---|---|
java.util.Set<?> |
allElements()
Returns all KeY-elements mapped by Recoder2KeY object of this
KeYProgModelInfo.
|
private ImmutableList<Field> |
asKeYFields(java.util.List<? extends Field> rfl)
returns the same fields as given in rfl and returns
their KeY representation
|
private ImmutableList<KeYJavaType> |
asKeYJavaTypes(java.util.List<ClassType> rctl)
returns a list of KeYJavaTypes representing the given recoder types in
the same order
|
KeYProgModelInfo |
copy() |
private Recoder2KeY |
createRecoder2KeY(NamespaceSet nss) |
private boolean |
declaresApplicableMethods(ClassType ct,
java.lang.String name,
java.util.List<Type> signature) |
ImmutableList<KeYJavaType> |
findImplementations(Type ct,
java.lang.String name,
ImmutableList<KeYJavaType> signature) |
ImmutableList<Field> |
getAllFieldsLocallyDeclaredIn(KeYJavaType ct)
returns the fields defined within the given class type.
|
ImmutableList<Method> |
getAllMethods(KeYJavaType kjt)
Returns all visible methods that are defined in this
class type or any of its supertypes.
|
ImmutableList<IProgramMethod> |
getAllProgramMethods(KeYJavaType kjt)
Returns all visible methods that are defined in this
class type or any of its supertypes.
|
ImmutableList<ProgramMethod> |
getAllProgramMethodsLocallyDeclared(KeYJavaType ct)
Returns the ProgramMethods locally defined within the given
class type.
|
private java.util.List<Method> |
getAllRecoderMethods(KeYJavaType kjt) |
private java.util.List<ClassType> |
getAllRecoderSubtypes(KeYJavaType ct)
returns all proper subtypes of class
ct (i.e. without ct itself) |
private java.util.List<ClassType> |
getAllRecoderSupertypes(KeYJavaType ct)
returns all supertypes of the given class type with the type itself as
first element
|
ImmutableList<KeYJavaType> |
getAllSubtypes(KeYJavaType ct)
Returns all proper subtypes of the given class type
|
ImmutableList<KeYJavaType> |
getAllSupertypes(KeYJavaType ct)
Returns all known supertypes of the given class type with the type itself
as first element.
|
ImmutableList<Field> |
getAllVisibleFields(KeYJavaType ct)
returns all in ct visible fields
declared in ct or one of its supertypes
in topological order starting with the fields of
the given type
If the type is represented in source code, the returned list
matches the syntactic order.
|
IProgramMethod |
getConstructor(KeYJavaType ct,
ImmutableList<KeYJavaType> signature)
retrieves the most specific constructor declared in the given type with
respect to the given signature
|
ImmutableList<IProgramMethod> |
getConstructors(KeYJavaType ct)
Returns the constructors locally defined within the given
class type.
|
KeYRecoderExcHandler |
getExceptionHandler() |
java.lang.String |
getFullName(KeYJavaType t)
Returns the full name of a KeYJavaType t.
|
private IProgramMethod |
getImplicitMethod(KeYJavaType ct,
java.lang.String name)
retrieves implicit methods
|
ImmutableList<Method> |
getMethods(KeYJavaType ct)
Returns the methods locally defined within the given
class type.
|
ImmutableList<Method> |
getMethods(KeYJavaType ct,
java.lang.String m,
ImmutableList<Type> signature,
KeYJavaType context)
Returns the list of most specific methods with the given
name that are defined in the given type or in a supertype
where they are visible for the given type, and have a signature
that is compatible to the given one.
|
IProgramMethod |
getProgramMethod(KeYJavaType ct,
java.lang.String m,
ImmutableList<? extends Type> signature,
KeYJavaType context)
Returns the IProgramMethods with the given name that is defined
in the given type or in a supertype where it is visible for the
given type, and has a signature that is compatible to the given one.
|
private java.util.List<? extends Constructor> |
getRecoderConstructors(KeYJavaType ct) |
private java.util.List<? extends Constructor> |
getRecoderConstructors(KeYJavaType ct,
ImmutableList<KeYJavaType> signature) |
private java.util.List<Method> |
getRecoderMethods(KeYJavaType kjt) |
private java.util.List<Method> |
getRecoderMethods(KeYJavaType ct,
java.lang.String m,
ImmutableList<? extends Type> signature,
KeYJavaType context) |
private java.util.List<Type> |
getRecoderTypes(ImmutableList<? extends Type> types) |
KeYCrossReferenceServiceConfiguration |
getServConf() |
Type |
getType(TypeReference tr) |
private ImmutableList<Field> |
getVisibleArrayFields(KeYJavaType arrayType)
returns all fields of and visible in an array field
|
private boolean |
isAssignmentCompatible(ArrayType subType,
ArrayType type)
checks whether subType is assignment compatible to type according
to the rules defined in the java language specification
|
private boolean |
isDeclaringInterface(ClassType ct,
java.lang.String name,
java.util.List<Type> signature) |
boolean |
isFinal(KeYJavaType kjt) |
boolean |
isPackage(java.lang.String name)
checks if name refers to a package
|
private boolean |
isSubtype(ClassType classSubType,
ClassType classType) |
boolean |
isSubtype(KeYJavaType subType,
KeYJavaType superType)
Checks whether subType is a subtype of superType or not.
|
private boolean |
isSubtype(Type subType,
Type superType) |
void |
putImplicitMethod(IProgramMethod m,
KeYJavaType t) |
JavaBlock |
readBlock(java.lang.String block,
ClassDeclaration cd,
NamespaceSet nss)
Parses a given JavaBlock using cd as context to determine the right
references.
|
JavaBlock |
readJavaBlock(java.lang.String block,
NamespaceSet nss)
Parses a given JavaBlock using an empty context.
|
KeYRecoderMapping |
rec2key() |
private ImmutableList<KeYJavaType> |
recFindImplementations(ClassType ct,
java.lang.String name,
java.util.List<Type> signature,
ImmutableList<KeYJavaType> result) |
KeYJavaType |
resolveType(java.lang.String shortName,
KeYJavaType context) |
private ClassType |
searchType(java.lang.String shortName,
java.util.List<? extends ClassType> types) |
private Services services
private KeYCrossReferenceServiceConfiguration sc
private KeYRecoderMapping mapping
private TypeConverter typeConverter
private java.util.HashMap<KeYJavaType,java.util.HashMap<java.lang.String,IProgramMethod>> implicits
private KeYRecoderExcHandler exceptionHandler
public KeYProgModelInfo(Services services, TypeConverter typeConverter, KeYRecoderExcHandler keh)
KeYProgModelInfo(Services services, KeYCrossReferenceServiceConfiguration crsc, KeYRecoderMapping krm, TypeConverter typeConverter)
public KeYRecoderMapping rec2key()
public KeYCrossReferenceServiceConfiguration getServConf()
public KeYRecoderExcHandler getExceptionHandler()
public java.util.Set<?> allElements()
private java.util.List<Method> getAllRecoderMethods(KeYJavaType kjt)
public ImmutableList<Method> getAllMethods(KeYJavaType kjt)
public ImmutableList<IProgramMethod> getAllProgramMethods(KeYJavaType kjt)
private java.util.List<Type> getRecoderTypes(ImmutableList<? extends Type> types)
public KeYJavaType resolveType(java.lang.String shortName, KeYJavaType context)
private ClassType searchType(java.lang.String shortName, java.util.List<? extends ClassType> types)
public java.lang.String getFullName(KeYJavaType t)
public Type getType(TypeReference tr)
public boolean isFinal(KeYJavaType kjt)
public boolean isSubtype(KeYJavaType subType, KeYJavaType superType)
public boolean isPackage(java.lang.String name)
name
- a String with the name to be checkedprivate boolean isAssignmentCompatible(ArrayType subType, ArrayType type)
private java.util.List<Method> getRecoderMethods(KeYJavaType kjt)
private java.util.List<? extends Constructor> getRecoderConstructors(KeYJavaType ct)
private java.util.List<Method> getRecoderMethods(KeYJavaType ct, java.lang.String m, ImmutableList<? extends Type> signature, KeYJavaType context)
private java.util.List<? extends Constructor> getRecoderConstructors(KeYJavaType ct, ImmutableList<KeYJavaType> signature)
public ImmutableList<Method> getMethods(KeYJavaType ct, java.lang.String m, ImmutableList<Type> signature, KeYJavaType context)
ct
- the class type to get methods from.m
- the name of the methods in question.signature
- the statical type signature of a callee.public ImmutableList<Method> getMethods(KeYJavaType ct)
ct
- a class type.public ImmutableList<ProgramMethod> getAllProgramMethodsLocallyDeclared(KeYJavaType ct)
ct
- a class type.public ImmutableList<IProgramMethod> getConstructors(KeYJavaType ct)
ct
- a class type.public IProgramMethod getConstructor(KeYJavaType ct, ImmutableList<KeYJavaType> signature)
ct
- the KeYJavyType where to look for the constructorsignature
- IListprivate IProgramMethod getImplicitMethod(KeYJavaType ct, java.lang.String name)
public IProgramMethod getProgramMethod(KeYJavaType ct, java.lang.String m, ImmutableList<? extends Type> signature, KeYJavaType context)
ct
- the class type to get methods from.m
- the name of the methods in question.signature
- the statical type signature of a callee.private ImmutableList<Field> asKeYFields(java.util.List<? extends Field> rfl)
rfl
- the List of fields to be looked uppublic ImmutableList<Field> getAllFieldsLocallyDeclaredIn(KeYJavaType ct)
ct
- the class type whose fields are returnedpublic ImmutableList<Field> getAllVisibleFields(KeYJavaType ct)
ct
- the class type whose fields are returnedprivate ImmutableList<Field> getVisibleArrayFields(KeYJavaType arrayType)
arrayType
- the KeYJavaType of the arrayprivate java.util.List<ClassType> getAllRecoderSubtypes(KeYJavaType ct)
ct
(i.e. without ct
itself)private java.util.List<ClassType> getAllRecoderSupertypes(KeYJavaType ct)
private ImmutableList<KeYJavaType> asKeYJavaTypes(java.util.List<ClassType> rctl)
rctl
- the ASTListpublic ImmutableList<KeYJavaType> getAllSupertypes(KeYJavaType ct)
ct
- a class typepublic ImmutableList<KeYJavaType> getAllSubtypes(KeYJavaType ct)
ct
- a class typeprivate Recoder2KeY createRecoder2KeY(NamespaceSet nss)
public JavaBlock readBlock(java.lang.String block, ClassDeclaration cd, NamespaceSet nss)
block
- a String describing a java blockcd
- ClassDeclaration representing the context in which the
block has to be interpreted.public JavaBlock readJavaBlock(java.lang.String block, NamespaceSet nss)
block
- a String describing a java blockpublic ImmutableList<KeYJavaType> findImplementations(Type ct, java.lang.String name, ImmutableList<KeYJavaType> signature)
private ImmutableList<KeYJavaType> recFindImplementations(ClassType ct, java.lang.String name, java.util.List<Type> signature, ImmutableList<KeYJavaType> result)
private boolean declaresApplicableMethods(ClassType ct, java.lang.String name, java.util.List<Type> signature)
private boolean isDeclaringInterface(ClassType ct, java.lang.String name, java.util.List<Type> signature)
public void putImplicitMethod(IProgramMethod m, KeYJavaType t)
public KeYProgModelInfo copy()