public class KeYProgModelInfo
extends java.lang.Object
Constructor and Description |
---|
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.
|
KeYProgModelInfo |
copy() |
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.
|
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.
|
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.
|
KeYCrossReferenceServiceConfiguration |
getServConf() |
Type |
getType(TypeReference tr) |
boolean |
isFinal(KeYJavaType kjt) |
boolean |
isPackage(java.lang.String name)
checks if name refers to a package
|
boolean |
isSubtype(KeYJavaType subType,
KeYJavaType superType)
Checks whether subType is a subtype of superType or not.
|
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() |
KeYJavaType |
resolveType(java.lang.String shortName,
KeYJavaType context) |
public KeYProgModelInfo(Services services, TypeConverter typeConverter, KeYRecoderExcHandler keh)
public KeYRecoderMapping rec2key()
public KeYCrossReferenceServiceConfiguration getServConf()
public KeYRecoderExcHandler getExceptionHandler()
public java.util.Set<?> allElements()
public ImmutableList<Method> getAllMethods(KeYJavaType kjt)
public ImmutableList<IProgramMethod> getAllProgramMethods(KeYJavaType kjt)
public KeYJavaType resolveType(java.lang.String shortName, KeYJavaType context)
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 checkedpublic 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
- IListpublic 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.public 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 returnedpublic ImmutableList<KeYJavaType> getAllSupertypes(KeYJavaType ct)
ct
- a class typepublic ImmutableList<KeYJavaType> getAllSubtypes(KeYJavaType ct)
ct
- a class typepublic 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)
public void putImplicitMethod(IProgramMethod m, KeYJavaType t)
public KeYProgModelInfo copy()
Copyright © 2003-2019 The KeY-Project.