| java.lang.Object
 de.uka.ilkd.key.java.JavaInfo
| JavaInfo | | public class JavaInfo (Code) | | an instance serves as representation of a Java model underlying a DL
formula. This class provides calls to access the elements of the Java
model using the KeY datastructures only. Implementation specific
details like the use of Recoder is hidden in the field of type
KeYProgModelInfo . This class can be extended to provide further
services.
|
| Inner Class :public class CacheKey | |
| Inner Class :abstract static class Filter | |
| Method Summary | |
| public JavaInfo | copy(Services serv)
| | public ListOfKeYJavaType | createSignature(ArrayOfExpression arguments)
| | public TypeReference | createTypeReference(KeYJavaType kjt)
| | public ListOfProgramVariable | getAllAttributes(String programName, KeYJavaType type)
| | public ListOfField | getAllFields(ClassDeclaration classDecl)
retrieves all attributes locally declared in class cl
(inclusive the implicit attributes)
The returned list is in source code order. | | public Set | getAllKeYJavaTypes()
| | public ListOfMethod | getAllMethods(KeYJavaType kjt)
| | public ListOfProgramMethod | getAllProgramMethods(KeYJavaType kjt)
| | public ListOfProgramMethod | getAllProgramMethodsLocallyDeclared(KeYJavaType kjt)
| | public ListOfKeYJavaType | getAllSubtypes(KeYJavaType type)
| | public ListOfKeYJavaType | getAllSupertypes(KeYJavaType type)
| | public ProgramVariable | getArrayLength()
| | public ProgramVariable | getAttribute(String fullyQualifiedName)
returns the programvariable for the specified attribute. | | public ProgramVariable | getAttribute(String programName, String qualifiedClassName)
| | public ProgramVariable | getAttribute(String name, KeYJavaType classType)
| | public ProgramVariable | getAttribute(String attributeName, ObjectSort s)
| | public ListOfKeYJavaType | getCommonSubtypes(KeYJavaType k1, KeYJavaType k2)
returns the list of all common subtypes of types k1 and k2
(inclusive one of them if they are equal or subtypes themselves)
attention: Null is not a jav atype only a logic sort, i.e. | | public ExecutionContext | getDefaultExecutionContext()
returns the default execution context. | | public ListOfKeYJavaType | getDirectSuperTypes(KeYJavaType type)
| | public String | getFullName(KeYJavaType t)
returns the full name of a given
de.uka.ilkd.key.java.abstraction.KeYJavaType . | | public ListOfField | getImplicitFields(ClassDeclaration cl)
retrieves all implicit attributes locally declared in the given class
The returned list is in source code order. | | public Function | getInReachableState()
| | public KeYJavaType | getJavaIoSerializable()
| | public Sort | getJavaIoSerializableAsSort()
| | public KeYJavaType | getJavaLangCloneable()
| | public Sort | getJavaLangCloneableAsSort()
| | public KeYJavaType | getJavaLangObject()
| | public Sort | getJavaLangObjectAsSort()
| | public String | getJavaSourcePath()
| | public KeYJavaType | getKeYJavaType(String fullName)
| | public KeYJavaType | getKeYJavaType(Sort sort)
| | public KeYJavaType | getKeYJavaType(Type t)
| | public KeYJavaType | getKeYJavaTypeByClassName(String className)
| | public KeYProgModelInfo | getKeYProgModelInfo()
returns the underlying KeYProgModelInfo providing access to the
Recoder structures. | | public ListOfMethod | getMethods(KeYJavaType kjt)
| | public Term | getNullConst()
| | public Term | getNullTerm()
| | public KeYJavaType | getNullType()
| | public Namespace | getObjectSorts()
| | public KeYJavaType | getPrimitiveKeYJavaType(String typename)
returns a primitive KeYJavaType matching the given typename making use
of the LDTs of the current type converter in the services. | | public KeYJavaType | getPrimitiveKeYJavaType(Expression e)
| | public ProgramMethod | getProgramMethod(KeYJavaType classType, String methodName, ListOfType signature, KeYJavaType context)
| | public ProgramMethod | getProgramMethod(KeYJavaType ct, String methodName, ListOfKeYJavaType signature, KeYJavaType context)
| | public ProgramMethod | getProgramMethod(KeYJavaType classType, String methodName, ProgramVariable[] args, KeYJavaType context)
returns the program method defined in the KeYJavaType of the program
variable clv, with the name m, and the KeYJavaTypes of the given array
of program variables as signatures. | | public Term | getProgramMethodTerm(Term prefix, String methodName, Term[] args, String className)
| | public Services | getServices()
| | public KeYJavaType | getSuperclass(KeYJavaType type)
| | public KeYJavaType | getTypeByClassName(String className)
looks up a KeYJavaType with given name. | | public KeYJavaType | getTypeByName(String fullName)
| | public TypeDeclaration | getTypeDeclaration(String fullName)
| | public boolean | isAJavaCommonSort(Sort sort)
| | public boolean | isPackage(String name)
| | public boolean | isSubtype(KeYJavaType subType, KeYJavaType superType)
returns true iff the given subType KeYJavaType is a sub type of the
given KeYJavaType superType. | | public ProgramVariable | lookupVisibleAttribute(String programName, KeYJavaType classType)
looks up for a field of the given program name
visible in the specified class type belonging to the type
or one of its supertypes
Parameters:
programName - the String containing the name of the field to be looked up. | | public ProgramElement | readJava(String java)
| | public JavaBlock | readJavaBlock(String java, TypeDeclaration asIn)
reads a Java block given as a string java as it was in the given
TypeDeclaration asIn. | | public JavaBlock | readJavaBlock(String java)
| | public KeYRecoderMapping | rec2key()
| | public void | resetCaches()
| | public void | setJavaSourcePath(String path)
| | void | setKeYProgModelInfo(KeYProgModelInfo kpmi)
|
| DEFAULT_EXECUTION_CONTEXT_CLASS | | final static String DEFAULT_EXECUTION_CONTEXT_CLASS(Code) | | the name of the class used as default execution context
|
| copy | | public JavaInfo copy(Services serv)(Code) | | copies this JavaInfo and uses the given Services object as the
Services object of the copied JavaInfo
Parameters:
serv - the Services the copy will use and vice versa a copy of the JavaInfo |
| createSignature | | public ListOfKeYJavaType createSignature(ArrayOfExpression arguments)(Code) | | retrieves the signature according to the given expressions
Parameters:
arguments - ArrayOfExpression of which we try to construct asignature the signature |
| getAllAttributes | | public ListOfProgramVariable getAllAttributes(String programName, KeYJavaType type)(Code) | | returns a list of all attributes with the given program name
declared in one of type's sub- or supertype including
its own attributes
Attention:
The type must not denote the null type
Parameters:
programName - the String with name of the attribute as declared in a program
Parameters:
type - the KeYJavaType specifying the part of the hierarchy where to look for list of found attributes with name programName |
| getAllFields | | public ListOfField getAllFields(ClassDeclaration classDecl)(Code) | | retrieves all attributes locally declared in class cl
(inclusive the implicit attributes)
The returned list is in source code order.
Parameters:
classDecl - the ClassDeclaration whose attributes shall be collected all attributes declared in class cl |
| getAllKeYJavaTypes | | public Set getAllKeYJavaTypes()(Code) | | returns all known KeYJavaTypes of the current
program type model
all known KeYJavaTypes of the currentprogram type model |
| getAllMethods | | public ListOfMethod getAllMethods(KeYJavaType kjt)(Code) | | returns all methods from the given Type
|
| getAllProgramMethods | | public ListOfProgramMethod getAllProgramMethods(KeYJavaType kjt)(Code) | | returns all methods from the given Type as ProgramMethods
|
| getAllProgramMethodsLocallyDeclared | | public ListOfProgramMethod getAllProgramMethodsLocallyDeclared(KeYJavaType kjt)(Code) | | returns all methods declared in the given Type as ProgramMethods
|
| getAllSubtypes | | public ListOfKeYJavaType getAllSubtypes(KeYJavaType type)(Code) | | returns all proper subtypes of a given type
Parameters:
type - the KeYJavaType whose subtypes are returned list of all subtypes |
| getAllSupertypes | | public ListOfKeYJavaType getAllSupertypes(KeYJavaType type)(Code) | | returns all supertypes of a given type
Parameters:
type - the KeYJavaType whose supertypes are returned list of all supertypes |
| getAttribute | | public ProgramVariable getAttribute(String fullyQualifiedName)(Code) | | returns the programvariable for the specified attribute. The attribute
has to be fully qualified, i.e. declarationType::attributeName
Parameters:
fullyQualifiedName - the String with the fully qualified attribute name an attribute program variable of the given name
throws:
IllegalArgumentException - if the given name is not fully qualified |
| getAttribute | | public ProgramVariable getAttribute(String programName, String qualifiedClassName)(Code) | | returns the programvariable for the specified attribute declared in
the specified class
Parameters:
programName - the String with the name of the attribute
Parameters:
qualifiedClassName - the String with the full (inclusive package) qualifiedclass name the attribute program variable of the given name
throws:
IllegalArgumentException - if the qualified class name is empty ornull |
| getAttribute | | public ProgramVariable getAttribute(String name, KeYJavaType classType)(Code) | | returns the program variable representing the attribute of the given
name declared locally in class classType
the attribute of the given name declared in classType |
| getCommonSubtypes | | public ListOfKeYJavaType getCommonSubtypes(KeYJavaType k1, KeYJavaType k2)(Code) | | returns the list of all common subtypes of types k1 and k2
(inclusive one of them if they are equal or subtypes themselves)
attention: Null is not a jav atype only a logic sort, i.e.
if null is the only element shared between k1 and k2
the returned list will be empty
Parameters:
k1 - the first KeYJavaType denoting a class type
Parameters:
k2 - the second KeYJavaType denoting a classtype the list of common subtypes of types k1 and k2 |
| getDefaultExecutionContext | | public ExecutionContext getDefaultExecutionContext()(Code) | | returns the default execution context. This is equiavlent to executing the program
in a static method of a class placed in the default package
the default execution context |
| getDirectSuperTypes | | public ListOfKeYJavaType getDirectSuperTypes(KeYJavaType type)(Code) | | returns all direct supertypes (local declared types in extends and
implements) if extends is not given explict java.lang.Object is added
(it is not added for interfaces)
|
| getImplicitFields | | public ListOfField getImplicitFields(ClassDeclaration cl)(Code) | | retrieves all implicit attributes locally declared in the given class
The returned list is in source code order.
Parameters:
cl - the ClassDeclaration where to look for the implicitattributes all implicit attributes declared in cl |
| getInReachableState | | public Function getInReachableState()(Code) | | returns the predicate expressing that we are in a state reachable by executing a
a java program
|
| getJavaIoSerializable | | public KeYJavaType getJavaIoSerializable()(Code) | | returns the KeYJavaType for class java.io.Serializable
|
| getJavaIoSerializableAsSort | | public Sort getJavaIoSerializableAsSort()(Code) | | returns the KeYJavaType for class java.io.Serializable
|
| getJavaLangCloneable | | public KeYJavaType getJavaLangCloneable()(Code) | | returns the KeYJavaType for class java.lang.Clonable
|
| getJavaLangCloneableAsSort | | public Sort getJavaLangCloneableAsSort()(Code) | | returns the KeYJavaType for class java.lang.Cloneable
|
| getJavaLangObject | | public KeYJavaType getJavaLangObject()(Code) | | returns the KeYJavaType for class java.lang.Object
|
| getJavaLangObjectAsSort | | public Sort getJavaLangObjectAsSort()(Code) | | returns the KeYJavaType for class java.lang.Object
|
| getKeYJavaType | | public KeYJavaType getKeYJavaType(String fullName)(Code) | | returns a KeYJavaType (either primitive of object type) having the
full name of the given String fullName
Parameters:
fullName - a String with the type name to lookup |
| getKeYJavaType | | public KeYJavaType getKeYJavaType(Sort sort)(Code) | | returns a KeYJavaType having the given sort
|
| getKeYJavaType | | public KeYJavaType getKeYJavaType(Type t)(Code) | | returns the KeYJavaType belonging to the given Type t
|
| getKeYJavaTypeByClassName | | public KeYJavaType getKeYJavaTypeByClassName(String className)(Code) | | this is an alias for getTypeByClassName
|
| getKeYProgModelInfo | | public KeYProgModelInfo getKeYProgModelInfo()(Code) | | returns the underlying KeYProgModelInfo providing access to the
Recoder structures.
|
| getMethods | | public ListOfMethod getMethods(KeYJavaType kjt)(Code) | | returns all locally declared methods from the given Type
|
| getNullConst | | public Term getNullConst()(Code) | | returns a term representing the null constant in logic
|
| getNullTerm | | public Term getNullTerm()(Code) | | returns a term representing 'null' in logic
|
| getNullType | | public KeYJavaType getNullType()(Code) | | returns the KeYJavaType representing the type of 'null'
|
| getObjectSorts | | public Namespace getObjectSorts()(Code) | | returns all ObjectSorts of the underlying Java model
a namespace containing the object sorts |
| getPrimitiveKeYJavaType | | public KeYJavaType getPrimitiveKeYJavaType(String typename)(Code) | | returns a primitive KeYJavaType matching the given typename making use
of the LDTs of the current type converter in the services.
|
| getPrimitiveKeYJavaType | | public KeYJavaType getPrimitiveKeYJavaType(Expression e)(Code) | | returns the KeYJavaType of the expression if it can be
determined else null is returned
|
| getProgramMethod | | public ProgramMethod getProgramMethod(KeYJavaType classType, String methodName, ListOfType signature, KeYJavaType context)(Code) | | returns the program methods defined in the given KeYJavaType with name
m and the list of types as signature of the method
Parameters:
classType - the KeYJavaType of the class where to look for the method
Parameters:
methodName - the name of the method
Parameters:
signature - a ListOfType with the arguments types
Parameters:
context - the KeYJavaType of the class context from wherethe method is called a matching program method |
| getProgramMethod | | public ProgramMethod getProgramMethod(KeYJavaType ct, String methodName, ListOfKeYJavaType signature, KeYJavaType context)(Code) | | returns the program methods defined in the given KeYJavaType with name
m and the list of types as signature of the method
Parameters:
ct - the KeYJavaType of the class where to look for the method
Parameters:
methodName - the name of the method
Parameters:
signature - a ListOfKeYJavaType with the arguments types
Parameters:
context - the KeYJavaType of the class context from wherethe method is called a matching program method |
| getProgramMethod | | public ProgramMethod getProgramMethod(KeYJavaType classType, String methodName, ProgramVariable[] args, KeYJavaType context)(Code) | | returns the program method defined in the KeYJavaType of the program
variable clv, with the name m, and the KeYJavaTypes of the given array
of program variables as signatures.
Parameters:
classType - the KeYJavaType of the class where to look for the method
Parameters:
methodName - the name of the method
Parameters:
args - an array of ProgramVariables as the arguments of the method
Parameters:
context - the KeYJavaType of the class context from wherethe method is called a matching program method |
| getServices | | public Services getServices()(Code) | | returns the services associated with this JavaInfo
|
| getSuperclass | | public KeYJavaType getSuperclass(KeYJavaType type)(Code) | | retrieves the direct extended superclass for the given class
Parameters:
type - the KeYJavaType of the type whose superclasshas to be determined KeYJavaType of the extended supertype |
| getTypeByClassName | | public KeYJavaType getTypeByClassName(String className)(Code) | | looks up a KeYJavaType with given name. If the name is a fully
qualifying name with package prefix an element with this full name is
taken. If the name does not contain a full package prefix some
KeYJavaType with this short name is taken.
Parameters:
className - the name to look for (either full or short) a class matching the name |
| getTypeByName | | public KeYJavaType getTypeByName(String fullName)(Code) | | looks up the fully qualifying name given by a String
in the list of all available
KeYJavaTypes in the Java model
Parameters:
fullName - the String the KeYJavaType with the name of the String |
| getTypeDeclaration | | public TypeDeclaration getTypeDeclaration(String fullName)(Code) | | returns a type declaration with the full name of the given String fullName
|
| isAJavaCommonSort | | public boolean isAJavaCommonSort(Sort sort)(Code) | | tests if sort represents java.lang.Object, java.lang.Cloneable or
java.io.Serializable
|
| isPackage | | public boolean isPackage(String name)(Code) | | checks if name refers to a package
Parameters:
name - a String with the name to be checked true iff name refers to a package |
| isSubtype | | public boolean isSubtype(KeYJavaType subType, KeYJavaType superType)(Code) | | returns true iff the given subType KeYJavaType is a sub type of the
given KeYJavaType superType.
|
| lookupVisibleAttribute | | public ProgramVariable lookupVisibleAttribute(String programName, KeYJavaType classType)(Code) | | looks up for a field of the given program name
visible in the specified class type belonging to the type
or one of its supertypes
Parameters:
programName - the String containing the name of the field to be looked up. The name is in short notation, i.e. not fully qualified
Parameters:
classType - the KeYJavaType of the class used as context the field of the given name |
| rec2key | | public KeYRecoderMapping rec2key()(Code) | | convenience method that returns the Recoder-to-KeY mapping underlying
the KeYProgModelInfo of this JavaInfo
|
| resetCaches | | public void resetCaches()(Code) | | |
| setJavaSourcePath | | public void setJavaSourcePath(String path)(Code) | | |
|
|