| java.lang.Object
 de.uka.ilkd.key.java.KeYProgModelInfo
| KeYProgModelInfo | | public class KeYProgModelInfo (Code) | | |
| Method Summary | |
| public Set | allElements()
Returns all KeY-elements mapped by Recoder2KeY object of this
KeYProgModelInfo. | | public Collection | allObjectSorts()
Returns all ObjectSorts mapped to java.Types in KeY. | | public KeYProgModelInfo | copy()
| | public ListOfKeYJavaType | findImplementations(Type ct, String name, ListOfKeYJavaType signature)
| | public ListOfField | getAllFieldsLocallyDeclaredIn(KeYJavaType ct)
returns the fields defined within the given class type. | | public ListOfMethod | getAllMethods(KeYJavaType kjt)
Returns all visible methods that are defined in this
class type or any of its supertypes. | | public ListOfProgramMethod | getAllProgramMethods(KeYJavaType kjt)
Returns all visible methods that are defined in this
class type or any of its supertypes. | | public ListOfProgramMethod | getAllProgramMethodsLocallyDeclared(KeYJavaType ct)
Returns the ProgramMethods locally defined within the given
class type. | | public ListOfKeYJavaType | getAllSubtypes(KeYJavaType ct)
| | public ListOfKeYJavaType | getAllSupertypes(KeYJavaType ct)
Returns all known subtypes of the given class type. | | public ListOfField | 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. | | public Constructor | getConstructor(KeYJavaType ct, ListOfKeYJavaType signature)
| | public ListOfProgramMethod | getConstructors(KeYJavaType ct)
Returns the constructors locally defined within the given
class type. | | public KeYExceptionHandler | getExceptionHandler()
| | public String | getFullName(KeYJavaType t)
Returns the full name of a KeYJavaType t. | | public ListOfMethod | getMethods(KeYJavaType ct, String m, ListOfType 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. | | public ListOfMethod | getMethods(KeYJavaType ct)
Returns the methods locally defined within the given
class type. | | public ProgramMethod | getProgramMethod(KeYJavaType ct, String m, ListOfType signature, KeYJavaType context)
Returns the programmethods 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.
In the case that no method has been found or that the method could not
be resolved uniquely null is returned. | | public ProgramMethod | getProgramMethod(KeYJavaType ct, String m, ListOfKeYJavaType signature, KeYJavaType context)
Returns the programmethods 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.
Parameters:
ct - the class type to get methods from.
Parameters:
m - the name of the methods in question.
Parameters:
signature - the statical type signature of a callee. | | public KeYCrossReferenceServiceConfiguration | getServConf()
| | public recoder.abstraction.Type | getType(TypeReference tr)
| | public boolean | isPackage(String name)
| | public boolean | isSubtype(KeYJavaType subType, KeYJavaType superType)
Checks whether subType is a subtype of superType or not. | | public void | putImplicitMethod(ProgramMethod m, KeYJavaType t)
| | public JavaBlock | readBlock(String block, ClassDeclaration cd, NamespaceSet nss)
Parses a given JavaBlock using cd as context to determine the right
references.
Parameters:
block - a String describing a java block
Parameters:
cd - ClassDeclaration representing the context in which theblock has to be interpreted. | | public JavaBlock | readJavaBlock(String block, NamespaceSet nss)
Parses a given JavaBlock using an empty context. | | public KeYRecoderMapping | rec2key()
|
| allElements | | public Set allElements()(Code) | | Returns all KeY-elements mapped by Recoder2KeY object of this
KeYProgModelInfo.
a Set object containing the KeY-elements. |
| allObjectSorts | | public Collection allObjectSorts()(Code) | | Returns all ObjectSorts mapped to java.Types in KeY.
a Collection containing the ObjectSorts. |
| findImplementations | | public ListOfKeYJavaType findImplementations(Type ct, String name, ListOfKeYJavaType signature)(Code) | | |
| getAllFieldsLocallyDeclaredIn | | public ListOfField getAllFieldsLocallyDeclaredIn(KeYJavaType ct)(Code) | | returns the fields defined within the given class type.
If the type is represented in source code, the returned list
matches the syntactic order.
Parameters:
ct - the class type whose fields are returned the list of field members of the given type. |
| getAllMethods | | public ListOfMethod getAllMethods(KeYJavaType kjt)(Code) | | Returns all visible methods that are defined in this
class type or any of its supertypes. The methods are
in topological order with respect to the inheritance hierarchy.
the list of visible methods of this type and its supertypes. |
| getAllProgramMethods | | public ListOfProgramMethod getAllProgramMethods(KeYJavaType kjt)(Code) | | Returns all visible methods that are defined in this
class type or any of its supertypes. The methods are
in topological order with respect to the inheritance hierarchy.
the list of visible methods of this type and its supertypes. |
| getAllProgramMethodsLocallyDeclared | | public ListOfProgramMethod getAllProgramMethodsLocallyDeclared(KeYJavaType ct)(Code) | | Returns the ProgramMethods locally defined within the given
class type. If the type is represented in source code,
the returned list matches the syntactic order.
Parameters:
ct - a class type. |
| getAllSubtypes | | public ListOfKeYJavaType getAllSubtypes(KeYJavaType ct)(Code) | | Returns all proper subtypes of the given class type
Parameters:
ct - a class type the list of the known subtypes of the given class type. |
| getAllSupertypes | | public ListOfKeYJavaType getAllSupertypes(KeYJavaType ct)(Code) | | Returns all known subtypes of the given class type.
Parameters:
ct - a class type the list of the known subtypes of the given class type. |
| getAllVisibleFields | | public ListOfField getAllVisibleFields(KeYJavaType ct)(Code) | | 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.
Parameters:
ct - the class type whose fields are returned the list of field members of the given type. |
| getConstructor | | public Constructor getConstructor(KeYJavaType ct, ListOfKeYJavaType signature)(Code) | | retrieves the most specific constructor declared in the given type with
respect to the given signature
Parameters:
ct - the KeYJavyType where to look for the constructor
Parameters:
signature - ListOfKeYJavaType representing the signature of the constructor the most specific constructor declared in the given type |
| getConstructors | | public ListOfProgramMethod getConstructors(KeYJavaType ct)(Code) | | Returns the constructors locally defined within the given
class type. If the type is represented in source code,
the returned list matches the syntactic order.
Parameters:
ct - a class type. |
| getFullName | | public String getFullName(KeYJavaType t)(Code) | | Returns the full name of a KeYJavaType t.
the full name of t as a String. |
| getMethods | | public ListOfMethod getMethods(KeYJavaType ct, String m, ListOfType signature, KeYJavaType context)(Code) | | 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. If used to resolve a
method call, the result should be defined and unambiguous.
Parameters:
ct - the class type to get methods from.
Parameters:
m - the name of the methods in question.
Parameters:
signature - the statical type signature of a callee. |
| getMethods | | public ListOfMethod getMethods(KeYJavaType ct)(Code) | | Returns the methods locally defined within the given
class type. If the type is represented in source code,
the returned list matches the syntactic order.
Parameters:
ct - a class type. |
| getProgramMethod | | public ProgramMethod getProgramMethod(KeYJavaType ct, String m, ListOfType signature, KeYJavaType context)(Code) | | Returns the programmethods 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.
In the case that no method has been found or that the method could not
be resolved uniquely null is returned.
Parameters:
ct - the class type to get methods from.
Parameters:
m - the name of the methods in question.
Parameters:
signature - the statical type signature of a callee. the programmethod, if one is found,null if none or more than one programmethod is found (in this casea debug output is written to console). |
| getProgramMethod | | public ProgramMethod getProgramMethod(KeYJavaType ct, String m, ListOfKeYJavaType signature, KeYJavaType context)(Code) | | Returns the programmethods 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.
Parameters:
ct - the class type to get methods from.
Parameters:
m - the name of the methods in question.
Parameters:
signature - the statical type signature of a callee. the programmethod, if one is found,null if none or more than one programmethod is found (in this casea debug output is written to console). |
| 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) | | Checks whether subType is a subtype of superType or not.
|
| readBlock | | public JavaBlock readBlock(String block, ClassDeclaration cd, NamespaceSet nss)(Code) | | Parses a given JavaBlock using cd as context to determine the right
references.
Parameters:
block - a String describing a java block
Parameters:
cd - ClassDeclaration representing the context in which theblock has to be interpreted. the parsed and resolved JavaBlock |
| readJavaBlock | | public JavaBlock readJavaBlock(String block, NamespaceSet nss)(Code) | | Parses a given JavaBlock using an empty context.
Parameters:
block - a String describing a java block the parsed and resolved JavaBlock |
|
|