Package | Description |
---|---|
de.uka.ilkd.key.gui |
This package contains classes forming the graphical user interface of KeY.
|
de.uka.ilkd.key.informationflow.po | |
de.uka.ilkd.key.informationflow.proof.init | |
de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
|
de.uka.ilkd.key.java.abstraction |
This package contains the meta model abstractions as used by the
semantical services.
|
de.uka.ilkd.key.java.declaration |
Elements of the Java syntax tree representing declarations.
|
de.uka.ilkd.key.java.expression |
Elements of the Java syntax tree representing expressions.
|
de.uka.ilkd.key.java.expression.literal |
This package contains representations for the various Java literal types.
|
de.uka.ilkd.key.java.expression.operator |
Elements of the Java syntax tree representing operators and operator-like
expressions.
|
de.uka.ilkd.key.java.expression.operator.adt | |
de.uka.ilkd.key.java.reference |
Elements of the Java syntax tree representing implicit or explicit (named)
references to other program elements.
|
de.uka.ilkd.key.java.statement |
Elements of the Java syntax tree representing pure statements.
|
de.uka.ilkd.key.logic |
provides a representation for the term and sequent
structure.
|
de.uka.ilkd.key.logic.op |
contains the operators of
Term s. |
de.uka.ilkd.key.nparser.builder | |
de.uka.ilkd.key.proof |
This package contains the core data structures of proofs, nodes, goals, as well
as machinery to deal with these data structures.
|
de.uka.ilkd.key.proof_references.analyst | |
de.uka.ilkd.key.proof.init |
This package contains classes handling prover initialisation.
|
de.uka.ilkd.key.proof.mgt |
This package contains classes for proof environments and proof management.
|
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.rule.metaconstruct |
contains classes representing the meta constructs of
Taclet s. |
de.uka.ilkd.key.rule.tacletbuilder | |
de.uka.ilkd.key.smt |
This package contains the SMT backend of KeY, allowing to translate KeY formulas
to formulas in formats such as SMT-LIB, and allowing to send such formulas to
SMT solvers such as Simplify or Z3.
|
de.uka.ilkd.key.speclang |
This package contains the specification language frontends of KeY.
|
de.uka.ilkd.key.speclang.jml | |
de.uka.ilkd.key.speclang.jml.translation | |
de.uka.ilkd.key.speclang.njml |
This package provides the functionalities of parsing JML comments into KeY constructs.
|
de.uka.ilkd.key.speclang.translation | |
de.uka.ilkd.key.symbolic_execution.model.impl | |
de.uka.ilkd.key.symbolic_execution.po | |
de.uka.ilkd.key.symbolic_execution.strategy.breakpoint | |
de.uka.ilkd.key.taclettranslation.lemma | |
de.uka.ilkd.key.testgen | |
de.uka.ilkd.key.util |
This package is a grab bag of miscellaneous useful code fragments.
|
Modifier and Type | Method and Description |
---|---|
void |
ClassTree.select(KeYJavaType kjt) |
void |
ClassTree.select(KeYJavaType kjt,
IObserverFunction target) |
static void |
ProofManagementDialog.showInstance(InitConfig initConfig,
KeYJavaType selectedKJT,
IObserverFunction selectedTarget)
Shows the dialog and selects the passed
KeYJavaType and its
IObserverFunction . |
Constructor and Description |
---|
ClassTree(boolean addContractTargets,
boolean skipLibraryClasses,
Services services,
java.util.Map<Pair<KeYJavaType,IObserverFunction>,javax.swing.Icon> targetIcons) |
Modifier and Type | Method and Description |
---|---|
protected KeYJavaType |
LoopInvExecutionPO.getCalleeKeYJavaType() |
protected KeYJavaType |
InfFlowContractPO.getCalleeKeYJavaType()
Returns the
KeYJavaType which contains AbstractOperationPO.getProgramMethod() . |
protected KeYJavaType |
BlockExecutionPO.getCalleeKeYJavaType()
Returns the
KeYJavaType which contains AbstractOperationPO.getProgramMethod() . |
protected KeYJavaType |
SymbolicExecutionPO.getCalleeKeYJavaType()
Returns the
KeYJavaType which contains AbstractOperationPO.getProgramMethod() . |
KeYJavaType |
InfFlowContractPO.getContainerType()
Returns the
KeYJavaType in which the proven element is contained in. |
KeYJavaType |
SymbolicExecutionPO.getContainerType()
Returns the
KeYJavaType in which the proven element is contained in. |
Modifier and Type | Method and Description |
---|---|
static StateVars |
StateVars.buildMethodContractPostVars(StateVars preVars,
IProgramMethod pm,
KeYJavaType kjt,
Services services) |
static StateVars |
StateVars.buildMethodContractPreVars(IProgramMethod pm,
KeYJavaType kjt,
Services services) |
Modifier and Type | Field and Description |
---|---|
protected KeYJavaType[] |
JavaInfo.commonTypes
as accessed very often caches:
KeYJavaType of
java.lang.Object, java.lang.Clonable, java.io.Serializable
in in this order
|
Modifier and Type | Method and Description |
---|---|
KeYJavaType |
TypeConverter.getBooleanType() |
KeYJavaType |
ConstantExpressionEvaluator.getCompileTimeConstantType(Expression expr) |
KeYJavaType |
JavaInfo.getJavaIoSerializable()
returns the KeYJavaType for class java.io.Serializable
|
KeYJavaType |
JavaInfo.getJavaLangCloneable()
returns the KeYJavaType for class java.lang.Clonable
|
KeYJavaType |
JavaInfo.getJavaLangObject()
returns the KeYJavaType for class java.lang.Object
|
KeYJavaType |
TypeConverter.getKeYJavaType(Expression e)
Retrieves the static type of the expression.
|
KeYJavaType |
TypeConverter.getKeYJavaType(Expression e,
ExecutionContext ec)
retrieves the type of the expression e with respect to
the context in which it is evaluated
|
KeYJavaType |
Expression.getKeYJavaType(Services javaServ,
ExecutionContext ec)
returns the
KeYJavaType of an expression |
KeYJavaType |
JavaInfo.getKeYJavaType(Sort sort)
returns a KeYJavaType having the given sort
|
KeYJavaType |
JavaInfo.getKeYJavaType(java.lang.String fullName)
returns a KeYJavaType (either primitive of object type) having the
full name of the given String fullName
|
KeYJavaType |
Recoder2KeYTypeConverter.getKeYJavaType(java.lang.String typeName)
return the corresponding KeY JavaType for a recoder type.
|
KeYJavaType |
TypeConverter.getKeYJavaType(Term t) |
KeYJavaType |
JavaInfo.getKeYJavaType(Type t)
returns the KeYJavaType belonging to the given Type t
|
KeYJavaType |
Recoder2KeYTypeConverter.getKeYJavaType(Type t)
return the corresponding KeY JavaType for a recoder type.
|
KeYJavaType |
TypeConverter.getKeYJavaType(Type t) |
KeYJavaType |
JavaInfo.getNullType()
returns the KeYJavaType representing the type of 'null'
|
KeYJavaType |
JavaInfo.getPrimitiveKeYJavaType(PrimitiveType type) |
KeYJavaType |
JavaInfo.getPrimitiveKeYJavaType(java.lang.String typename)
returns a primitive KeYJavaType matching the given typename.
|
KeYJavaType |
TypeConverter.getPromotedType(KeYJavaType type1) |
KeYJavaType |
TypeConverter.getPromotedType(KeYJavaType type1,
KeYJavaType type2)
performs binary numeric promotion on the argument types
|
KeYJavaType |
KeYRecoderMapping.getSuperArrayType() |
KeYJavaType |
JavaInfo.getSuperclass(KeYJavaType type)
retrieves the direct extended superclass for the given class
|
KeYJavaType |
JavaInfo.getTypeByClassName(java.lang.String className)
looks up a KeYJavaType with given name.
|
KeYJavaType |
JavaInfo.getTypeByClassName(java.lang.String name,
KeYJavaType containerType)
retrieves the KeYJavaType of the given type name.
|
KeYJavaType |
JavaInfo.getTypeByName(java.lang.String fullName)
looks up the fully qualifying name given by a String
in the list of all available
KeYJavaTypes in the Java model
|
KeYJavaType |
KeYProgModelInfo.resolveType(java.lang.String shortName,
KeYJavaType context) |
Modifier and Type | Method and Description |
---|---|
ImmutableList<KeYJavaType> |
JavaInfo.createSignature(ImmutableArray<? extends Expression> arguments)
retrieves the signature according to the given expressions
|
ImmutableList<KeYJavaType> |
KeYProgModelInfo.findImplementations(Type ct,
java.lang.String name,
ImmutableList<KeYJavaType> signature) |
java.util.Set<KeYJavaType> |
JavaInfo.getAllKeYJavaTypes()
returns all known KeYJavaTypes of the current
program type model
|
ImmutableList<KeYJavaType> |
JavaInfo.getAllSubtypes(KeYJavaType type)
returns all proper subtypes of a given type
|
ImmutableList<KeYJavaType> |
KeYProgModelInfo.getAllSubtypes(KeYJavaType ct)
Returns all proper subtypes of the given class type
|
ImmutableList<KeYJavaType> |
JavaInfo.getAllSupertypes(KeYJavaType type)
returns all supertypes of a given type
|
ImmutableList<KeYJavaType> |
KeYProgModelInfo.getAllSupertypes(KeYJavaType ct)
Returns all known supertypes of the given class type with the type itself
as first element.
|
ImmutableList<KeYJavaType> |
JavaInfo.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.
|
ImmutableList<KeYJavaType> |
JavaInfo.getDirectSuperTypes(KeYJavaType type)
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)
|
java.util.List<KeYJavaType> |
JavaInfo.lookupSort2KJTCache(Sort sort) |
Modifier and Type | Method and Description |
---|---|
static ArrayInitializer |
KeYJavaASTFactory.arrayInitializer(Expression[] expressions,
KeYJavaType type)
Create an array initializer.
|
static TypeCast |
KeYJavaASTFactory.cast(Expression expression,
KeYJavaType targetType) |
static Catch |
KeYJavaASTFactory.catchClause(JavaInfo javaInfo,
java.lang.String param,
KeYJavaType kjt,
StatementBlock body)
Create a catch clause.
|
ArrayDeclaration |
Recoder2KeYTypeConverter.createArrayType(KeYJavaType baseType,
KeYJavaType arrayType)
create
|
TypeReference |
JavaInfo.createTypeReference(KeYJavaType kjt)
creates a new TypeReference for the given KeYJavaType
|
static LocalVariableDeclaration |
KeYJavaASTFactory.declare(ImmutableArray<Modifier> modifiers,
IProgramVariable variable,
Expression init,
KeYJavaType type)
Create a local variable declaration with an arbitrary number of
modifiers.
|
static ProgramElement |
KeYJavaASTFactory.declare(ImmutableArray<Modifier> modifiers,
IProgramVariable variable,
Expression init,
ProgramElementName typeName,
int dimensions,
ReferencePrefix typePrefix,
KeYJavaType baseType)
Create a local array variable declaration with an arbitrary number of
modifiers.
|
static LocalVariableDeclaration |
KeYJavaASTFactory.declare(IProgramVariable var,
Expression init,
KeYJavaType type)
Create a local variable declaration.
|
static LocalVariableDeclaration |
KeYJavaASTFactory.declare(IProgramVariable var,
KeYJavaType type)
Create a local variable declaration without initialization.
|
static LocalVariableDeclaration |
KeYJavaASTFactory.declare(Modifier[] modifiers,
IProgramVariable variable,
Expression init,
KeYJavaType type)
Create a local variable declaration with an arbitrary number of
modifiers.
|
static LocalVariableDeclaration |
KeYJavaASTFactory.declare(Modifier modifier,
IProgramVariable variable,
Expression init,
KeYJavaType type)
Create a local variable declaration with a single modifier.
|
static LocalVariableDeclaration |
KeYJavaASTFactory.declare(ProgramElementName name,
Expression init,
KeYJavaType type)
create a local variable declaration
type name = init; |
static LocalVariableDeclaration |
KeYJavaASTFactory.declare(ProgramElementName name,
KeYJavaType type)
Create a local variable declaration without initialization.
|
static LocalVariableDeclaration |
KeYJavaASTFactory.declare(Services services,
java.lang.String name,
Expression initializer,
KeYJavaType type)
Create a local variable declaration with a unique name.
|
static LocalVariableDeclaration |
KeYJavaASTFactory.declare(java.lang.String name,
KeYJavaType type)
create a local variable declaration
|
static LocalVariableDeclaration |
KeYJavaASTFactory.declareMethodCall(KeYJavaType type,
IProgramVariable variable,
ReferencePrefix reference,
java.lang.String method)
Create a local variable declaration that assigns a method's return value
initially.
|
static LocalVariableDeclaration |
KeYJavaASTFactory.declareZero(KeYJavaType type,
IProgramVariable variable)
Create a local variable declaration that assigns zero initially.
|
static ExecutionContext |
KeYJavaASTFactory.executionContext(KeYJavaType classType,
IProgramMethod method,
ReferencePrefix reference)
Create an execution context.
|
Term |
TypeConverter.findThisForSort(Sort s,
Term self,
KeYJavaType context,
boolean exact) |
ImmutableList<ProgramVariable> |
JavaInfo.getAllAttributes(java.lang.String programName,
KeYJavaType type) |
ImmutableList<ProgramVariable> |
JavaInfo.getAllAttributes(java.lang.String programName,
KeYJavaType type,
boolean traverseSubtypes)
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
|
ImmutableList<Field> |
KeYProgModelInfo.getAllFieldsLocallyDeclaredIn(KeYJavaType ct)
returns the fields defined within the given class type.
|
ImmutableList<Method> |
JavaInfo.getAllMethods(KeYJavaType kjt)
returns all methods from the given Type
|
ImmutableList<Method> |
KeYProgModelInfo.getAllMethods(KeYJavaType kjt)
Returns all visible methods that are defined in this
class type or any of its supertypes.
|
ImmutableList<IProgramMethod> |
JavaInfo.getAllProgramMethods(KeYJavaType kjt)
returns all methods from the given Type as IProgramMethods
|
ImmutableList<IProgramMethod> |
KeYProgModelInfo.getAllProgramMethods(KeYJavaType kjt)
Returns all visible methods that are defined in this
class type or any of its supertypes.
|
ImmutableList<ProgramMethod> |
JavaInfo.getAllProgramMethodsLocallyDeclared(KeYJavaType kjt)
returns all methods declared in the given Type as IProgramMethods
|
ImmutableList<ProgramMethod> |
KeYProgModelInfo.getAllProgramMethodsLocallyDeclared(KeYJavaType ct)
Returns the ProgramMethods locally defined within the given
class type.
|
ImmutableList<KeYJavaType> |
JavaInfo.getAllSubtypes(KeYJavaType type)
returns all proper subtypes of a given type
|
ImmutableList<KeYJavaType> |
KeYProgModelInfo.getAllSubtypes(KeYJavaType ct)
Returns all proper subtypes of the given class type
|
ImmutableList<KeYJavaType> |
JavaInfo.getAllSupertypes(KeYJavaType type)
returns all supertypes of a given type
|
ImmutableList<KeYJavaType> |
KeYProgModelInfo.getAllSupertypes(KeYJavaType ct)
Returns all known supertypes of the given class type with the type itself
as first element.
|
ImmutableList<Field> |
KeYProgModelInfo.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.
|
ProgramVariable |
JavaInfo.getAttribute(java.lang.String name,
KeYJavaType classType)
returns the program variable representing the attribute of the given
name declared locally in class classType
|
ProgramVariable |
JavaInfo.getCanonicalFieldProgramVariable(java.lang.String fieldName,
KeYJavaType kjt) |
ImmutableList<KeYJavaType> |
JavaInfo.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.
|
IProgramMethod |
JavaInfo.getConstructor(KeYJavaType kjt,
ImmutableList<KeYJavaType> signature) |
IProgramMethod |
KeYProgModelInfo.getConstructor(KeYJavaType ct,
ImmutableList<KeYJavaType> signature)
retrieves the most specific constructor declared in the given type with
respect to the given signature
|
ImmutableList<IProgramMethod> |
JavaInfo.getConstructors(KeYJavaType kjt) |
ImmutableList<IProgramMethod> |
KeYProgModelInfo.getConstructors(KeYJavaType ct)
Returns the constructors locally defined within the given
class type.
|
ImmutableList<KeYJavaType> |
JavaInfo.getDirectSuperTypes(KeYJavaType type)
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)
|
java.lang.String |
JavaInfo.getFullName(KeYJavaType t)
returns the full name of a given
KeYJavaType . |
java.lang.String |
KeYProgModelInfo.getFullName(KeYJavaType t)
Returns the full name of a KeYJavaType t.
|
ImmutableList<Method> |
JavaInfo.getMethods(KeYJavaType kjt)
returns all locally declared methods from the given Type
|
ImmutableList<Method> |
KeYProgModelInfo.getMethods(KeYJavaType ct)
Returns the methods locally defined within the given
class type.
|
ImmutableList<Method> |
KeYProgModelInfo.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 |
JavaInfo.getProgramMethod(KeYJavaType classType,
java.lang.String methodName,
ImmutableArray<? extends Type> signature,
KeYJavaType context) |
IProgramMethod |
JavaInfo.getProgramMethod(KeYJavaType classType,
java.lang.String methodName,
ImmutableList<? extends Type> signature,
KeYJavaType context)
returns the program methods defined in the given KeYJavaType with name
m and the list of types as signature of the method
|
IProgramMethod |
KeYProgModelInfo.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.
|
IProgramMethod |
JavaInfo.getProgramMethod(KeYJavaType classType,
java.lang.String methodName,
java.util.List<java.util.List<KeYJavaType>> signature,
KeYJavaType context) |
IProgramMethod |
JavaInfo.getProgramMethod(KeYJavaType classType,
java.lang.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.
|
KeYJavaType |
TypeConverter.getPromotedType(KeYJavaType type1) |
KeYJavaType |
TypeConverter.getPromotedType(KeYJavaType type1,
KeYJavaType type2)
performs binary numeric promotion on the argument types
|
IObserverFunction |
JavaInfo.getStaticInv(KeYJavaType target)
Returns the special symbol
<staticInv> which stands for the static invariant of a type. |
KeYJavaType |
JavaInfo.getSuperclass(KeYJavaType type)
retrieves the direct extended superclass for the given class
|
IProgramMethod |
JavaInfo.getToplevelPM(KeYJavaType kjt,
IProgramMethod pm) |
IProgramMethod |
JavaInfo.getToplevelPM(KeYJavaType kjt,
java.lang.String methodName,
ImmutableList<KeYJavaType> sig) |
KeYJavaType |
JavaInfo.getTypeByClassName(java.lang.String name,
KeYJavaType containerType)
retrieves the KeYJavaType of the given type name.
|
static Instanceof |
KeYJavaASTFactory.instanceOf(Expression expression,
KeYJavaType type)
Create an instance of operator.
|
boolean |
JavaInfo.isCanonicalProgramMethod(IProgramMethod method,
KeYJavaType context)
This is used for pretty printing observer terms.
|
boolean |
JavaInfo.isFinal(KeYJavaType kjt)
Checks whether the type is declared as final.
|
boolean |
KeYProgModelInfo.isFinal(KeYJavaType kjt) |
boolean |
JavaInfo.isInterface(KeYJavaType t) |
boolean |
TypeConverter.isNarrowing(KeYJavaType from,
KeYJavaType to) |
static boolean |
JavaInfo.isPrivate(KeYJavaType kjt) |
boolean |
JavaInfo.isSubtype(KeYJavaType subType,
KeYJavaType superType)
returns true iff the given subType KeYJavaType is a sub type of the
given KeYJavaType superType.
|
boolean |
KeYProgModelInfo.isSubtype(KeYJavaType subType,
KeYJavaType superType)
Checks whether subType is a subtype of superType or not.
|
static boolean |
JavaInfo.isVisibleTo(SpecificationElement ax,
KeYJavaType visibleTo) |
boolean |
TypeConverter.isWidening(KeYJavaType from,
KeYJavaType to) |
static ProgramVariable |
KeYJavaASTFactory.localVariable(ProgramElementName name,
KeYJavaType kjt)
create a local variable
|
static ProgramVariable |
KeYJavaASTFactory.localVariable(Services services,
java.lang.String name,
KeYJavaType type)
Create a local variable with a unique name.
|
static ProgramVariable |
KeYJavaASTFactory.localVariable(java.lang.String name,
KeYJavaType kjt)
create a local variable
|
ProgramVariable |
JavaInfo.lookupVisibleAttribute(java.lang.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
|
static ILoopInit |
KeYJavaASTFactory.loopInitZero(KeYJavaType type,
IProgramVariable variable)
Create a loop initialization that declares and assigns zero to a local
variable.
|
static MethodBodyStatement |
KeYJavaASTFactory.methodBody(JavaInfo model,
ProgramVariable result,
ReferencePrefix reference,
KeYJavaType classType,
java.lang.String methodName,
ProgramVariable[] arguments)
Create a method body shortcut.
|
static MethodReference |
KeYJavaASTFactory.methodCall(KeYJavaType type,
java.lang.String name)
Create a method call on a type with no arguments.
|
static MethodReference |
KeYJavaASTFactory.methodCall(KeYJavaType type,
java.lang.String name,
Expression... args)
Create a method call on a type.
|
static MethodReference |
KeYJavaASTFactory.methodCall(KeYJavaType type,
java.lang.String name,
ImmutableArray<? extends Expression> args)
Create a method call on a type.
|
static NewArray |
KeYJavaASTFactory.newArray(TypeReference typeRef,
int dimensions,
ArrayInitializer initializer,
KeYJavaType keyJavaType)
Create an array instantiation.
|
static NewArray |
KeYJavaASTFactory.newArray(TypeReference typeRef,
int dimensions,
Expression[] sizes,
ArrayInitializer initializer,
KeYJavaType keyJavaType)
Create an array instantiation.
|
static NewArray |
KeYJavaASTFactory.newArray(TypeReference typeRef,
int dimensions,
Expression[] sizes,
KeYJavaType keyJavaType)
Create an array instantiation.
|
static NewArray |
KeYJavaASTFactory.newArray(TypeReference typeRef,
int dimensions,
Expression size,
KeYJavaType keyJavaType)
Create an array instantiation.
|
static New |
KeYJavaASTFactory.newOperator(KeYJavaType type)
Create an object allocation without arguments.
|
static New |
KeYJavaASTFactory.newOperator(ReferencePrefix referencePrefix,
KeYJavaType type)
Create an object allocation without arguments.
|
static New |
KeYJavaASTFactory.newOperator(ReferencePrefix referencePrefix,
KeYJavaType type,
Expression[] args)
Create an object allocation.
|
static ParameterDeclaration |
KeYJavaASTFactory.parameterDeclaration(JavaInfo javaInfo,
KeYJavaType kjt,
IProgramVariable var)
Create a parameter declaration.
|
static ParameterDeclaration |
KeYJavaASTFactory.parameterDeclaration(JavaInfo javaInfo,
KeYJavaType kjt,
java.lang.String name)
create a parameter declaration
|
void |
KeYProgModelInfo.putImplicitMethod(IProgramMethod m,
KeYJavaType t) |
KeYJavaType |
KeYProgModelInfo.resolveType(java.lang.String shortName,
KeYJavaType context) |
void |
KeYRecoderMapping.setSuperArrayType(KeYJavaType superArrayType) |
static TypeRef |
KeYJavaASTFactory.typeRef(KeYJavaType type)
Create a type reference.
|
static TypeRef |
KeYJavaASTFactory.typeRef(KeYJavaType type,
int dimensions)
Create a type reference.
|
static VariableSpecification |
KeYJavaASTFactory.variableSpecification(IProgramVariable variable,
Expression initializer,
KeYJavaType keyJavaType)
Create a variable specification.
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<KeYJavaType> |
KeYProgModelInfo.findImplementations(Type ct,
java.lang.String name,
ImmutableList<KeYJavaType> signature) |
IProgramMethod |
JavaInfo.getConstructor(KeYJavaType kjt,
ImmutableList<KeYJavaType> signature) |
IProgramMethod |
KeYProgModelInfo.getConstructor(KeYJavaType ct,
ImmutableList<KeYJavaType> signature)
retrieves the most specific constructor declared in the given type with
respect to the given signature
|
IProgramMethod |
JavaInfo.getProgramMethod(KeYJavaType classType,
java.lang.String methodName,
java.util.List<java.util.List<KeYJavaType>> signature,
KeYJavaType context) |
IProgramMethod |
JavaInfo.getToplevelPM(KeYJavaType kjt,
java.lang.String methodName,
ImmutableList<KeYJavaType> sig) |
Constructor and Description |
---|
CreateArrayMethodBuilder(KeYJavaType integerType,
KeYJavaType objectType,
Sort heapSort,
int heapCount)
create the method builder for array implict creation methods
|
Modifier and Type | Class and Description |
---|---|
static class |
KeYJavaType.LexicographicalKeYJavaTypeOrder<T extends KeYJavaType> |
Modifier and Type | Field and Description |
---|---|
static KeYJavaType |
KeYJavaType.VOID_TYPE
Special return "type" for void methods.
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<KeYJavaType> |
NullType.getSupertypes()
Returns the array of locally declared supertypes of this class type.
|
ImmutableList<KeYJavaType> |
ClassType.getSupertypes()
Returns the array of locally declared supertypes of this class type.
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<KeYJavaType> |
InterfaceDeclaration.getSupertypes()
returns the local declared supertypes
|
ImmutableList<KeYJavaType> |
ArrayDeclaration.getSupertypes()
returns the local declared supertypes
|
abstract ImmutableList<KeYJavaType> |
TypeDeclaration.getSupertypes()
returns the local declared supertypes
|
ImmutableList<KeYJavaType> |
ClassDeclaration.getSupertypes()
returns the local declared supertypes
|
ImmutableList<KeYJavaType> |
SuperArrayDeclaration.getSupertypes()
returns the local declared supertypes
|
Constructor and Description |
---|
ArrayDeclaration(ExtList children,
TypeReference baseType,
KeYJavaType superType)
ArrayDeclaration
|
Modifier and Type | Field and Description |
---|---|
protected KeYJavaType |
ArrayInitializer.kjt |
Modifier and Type | Method and Description |
---|---|
abstract KeYJavaType |
Literal.getKeYJavaType(Services javaServ)
retrieves the literal's type
|
KeYJavaType |
Assignment.getKeYJavaType(Services javaServ,
ExecutionContext ec)
retrieves the type of the assignment expression
|
KeYJavaType |
ArrayInitializer.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
KeYJavaType |
Literal.getKeYJavaType(Services javaServ,
ExecutionContext ec)
retrieves the literal's type (as it is independant of the
execution context, it is same as using
Literal.getKeYJavaType(Services) ) |
abstract KeYJavaType |
Operator.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
KeYJavaType |
ParenthesizedExpression.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
Constructor and Description |
---|
ArrayInitializer(Expression[] expressions,
KeYJavaType kjt)
create a new array initializer with the given expressions as elements.
|
ArrayInitializer(ExtList list,
KeYJavaType kjt)
Array initializer.
|
Modifier and Type | Method and Description |
---|---|
KeYJavaType |
EmptySeqLiteral.getKeYJavaType(Services javaServ) |
KeYJavaType |
StringLiteral.getKeYJavaType(Services javaServ) |
KeYJavaType |
DoubleLiteral.getKeYJavaType(Services javaServ) |
KeYJavaType |
NullLiteral.getKeYJavaType(Services javaServ) |
KeYJavaType |
CharLiteral.getKeYJavaType(Services javaServ) |
KeYJavaType |
EmptySetLiteral.getKeYJavaType(Services javaServ) |
KeYJavaType |
RealLiteral.getKeYJavaType(Services javaServ) |
KeYJavaType |
FloatLiteral.getKeYJavaType(Services javaServ) |
KeYJavaType |
BooleanLiteral.getKeYJavaType(Services javaServ) |
KeYJavaType |
IntLiteral.getKeYJavaType(Services javaServ) |
KeYJavaType |
FreeLiteral.getKeYJavaType(Services javaServ) |
KeYJavaType |
LongLiteral.getKeYJavaType(Services javaServ) |
KeYJavaType |
EmptyMapLiteral.getKeYJavaType(Services javaServ) |
Modifier and Type | Method and Description |
---|---|
void |
DLEmbeddedExpression.check(Services javaServ,
KeYJavaType containingClass) |
Constructor and Description |
---|
NewArray(Expression[] arguments,
TypeReference typeRef,
KeYJavaType keyJavaType,
ArrayInitializer init,
int dimensions)
New array.
|
NewArray(ExtList children,
KeYJavaType keyJavaType,
ArrayInitializer init,
int dimensions)
New array.
|
Modifier and Type | Method and Description |
---|---|
KeYJavaType |
SeqIndexOf.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
KeYJavaType |
SeqSingleton.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
KeYJavaType |
SeqReverse.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
KeYJavaType |
SeqGet.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
KeYJavaType |
AllFields.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
KeYJavaType |
AllObjects.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
KeYJavaType |
SeqLength.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
KeYJavaType |
SeqSub.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
KeYJavaType |
Singleton.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
Modifier and Type | Method and Description |
---|---|
ImmutableList<KeYJavaType> |
MethodReference.getMethodSignature(Services services,
ExecutionContext ec)
determines the arguments types and constructs a signature of the current
method
|
Modifier and Type | Method and Description |
---|---|
IProgramMethod |
MethodReference.method(Services services,
KeYJavaType refPrefixType,
ExecutionContext ec) |
IProgramMethod |
MethodReference.method(Services services,
KeYJavaType classType,
ImmutableList<KeYJavaType> signature,
KeYJavaType context) |
Modifier and Type | Method and Description |
---|---|
IProgramMethod |
MethodReference.method(Services services,
KeYJavaType classType,
ImmutableList<KeYJavaType> signature,
KeYJavaType context) |
Constructor and Description |
---|
TypeRef(ExtList children,
KeYJavaType kjt,
int dim) |
TypeRef(KeYJavaType kjt)
creates a type reference for the given KeYJavaType with
dimension 0 and creates a suitable package reference prefix
from the KeYJavaType.
|
TypeRef(KeYJavaType kjt,
int dim)
creates a type reference for the given KeYJavaType and the
given dimension and creates a suitable package reference prefix
from the KeYJavaType.
|
TypeRef(ProgramElementName name,
int dimension,
ReferencePrefix prefix,
KeYJavaType kjt) |
Modifier and Type | Method and Description |
---|---|
KeYJavaType |
MethodBodyStatement.getBodySource() |
Modifier and Type | Method and Description |
---|---|
Term |
TermBuilder.reachableValue(Term t,
KeYJavaType kjt) |
Term |
TermBuilder.reachableValue(Term h,
Term t,
KeYJavaType kjt) |
LocationVariable |
TermBuilder.selfVar(IProgramMethod pm,
KeYJavaType kjt,
boolean makeNameUnique)
Creates a program variable for "self".
|
LocationVariable |
TermBuilder.selfVar(IProgramMethod pm,
KeYJavaType kjt,
boolean makeNameUnique,
java.lang.String postfix)
Creates a program variable for "self".
|
LocationVariable |
TermBuilder.selfVar(KeYJavaType kjt,
boolean makeNameUnique)
Creates a program variable for "self".
|
LocationVariable |
TermBuilder.selfVar(KeYJavaType kjt,
boolean makeNameUnique,
java.lang.String postfix)
Creates a program variable for "self".
|
Term |
TermBuilder.staticInv(KeYJavaType t) |
Term |
TermBuilder.staticInv(Term[] h,
KeYJavaType t) |
Modifier and Type | Method and Description |
---|---|
KeYJavaType |
ProgramVariable.getContainerType()
returns the KeYJavaType where the program variable is declared or
null if the program variable denotes not a field
|
KeYJavaType |
IObserverFunction.getContainerType()
Returns the container type of this symbol; for non-static observer
symbols, this corresponds to the sort of its second argument.
|
KeYJavaType |
ProgramSV.getContainerType() |
KeYJavaType |
ObserverFunction.getContainerType() |
KeYJavaType |
ProgramVariable.getKeYJavaType() |
KeYJavaType |
IProgramVariable.getKeYJavaType() |
KeYJavaType |
ProgramSV.getKeYJavaType() |
KeYJavaType |
ProgramVariable.getKeYJavaType(Services javaServ) |
KeYJavaType |
IProgramVariable.getKeYJavaType(Services javaServ) |
KeYJavaType |
ProgramSV.getKeYJavaType(Services javaServ) |
KeYJavaType |
ProgramVariable.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
KeYJavaType |
IProgramVariable.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
KeYJavaType |
ProgramSV.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
KeYJavaType |
ProgramMethod.getKJT()
Deprecated.
|
KeYJavaType |
ProgramMethod.getParameterType(int i) |
KeYJavaType |
IProgramMethod.getParameterType(int i)
returns the KeYJavaType of the i-th parameter declaration.
|
KeYJavaType |
ProgramSV.getParameterType(int i) |
KeYJavaType |
IObserverFunction.getParamType(int i)
Gives the type of the i-th parameter of this observer symbol.
|
KeYJavaType |
ProgramSV.getParamType(int i) |
KeYJavaType |
ObserverFunction.getParamType(int i) |
KeYJavaType |
ProgramMethod.getReturnType() |
KeYJavaType |
IProgramMethod.getReturnType() |
KeYJavaType |
ProgramSV.getReturnType() |
KeYJavaType |
IObserverFunction.getType()
Returns the result type of this symbol.
|
KeYJavaType |
ProgramSV.getType() |
KeYJavaType |
ObserverFunction.getType() |
Modifier and Type | Method and Description |
---|---|
ImmutableArray<KeYJavaType> |
IObserverFunction.getParamTypes()
Returns the parameter types of this observer symbol.
|
ImmutableArray<KeYJavaType> |
IProgramMethod.getParamTypes() |
ImmutableArray<KeYJavaType> |
ProgramSV.getParamTypes() |
ImmutableArray<KeYJavaType> |
ObserverFunction.getParamTypes() |
Modifier and Type | Method and Description |
---|---|
static ProgramElementName |
ObserverFunction.createName(java.lang.String baseName,
KeYJavaType container) |
Constructor and Description |
---|
LocationVariable(ProgramElementName name,
KeYJavaType t) |
LocationVariable(ProgramElementName name,
KeYJavaType t,
boolean isFinal) |
LocationVariable(ProgramElementName name,
KeYJavaType t,
boolean isGhost,
boolean isFinal) |
LocationVariable(ProgramElementName name,
KeYJavaType t,
KeYJavaType containingType,
boolean isStatic,
boolean isModel) |
LocationVariable(ProgramElementName name,
KeYJavaType t,
KeYJavaType containingType,
boolean isStatic,
boolean isModel,
boolean isGhost,
boolean isFinal) |
ObserverFunction(java.lang.String baseName,
Sort sort,
KeYJavaType type,
Sort heapSort,
KeYJavaType container,
boolean isStatic,
ImmutableArray<KeYJavaType> paramTypes,
int heapCount,
int stateCount) |
ProgramConstant(ProgramElementName name,
KeYJavaType t,
KeYJavaType containingType,
boolean isStatic,
Literal compileTimeConstant) |
ProgramMethod(MethodDeclaration method,
KeYJavaType container,
KeYJavaType kjt,
PositionInfo pi,
Sort heapSort) |
ProgramMethod(MethodDeclaration method,
KeYJavaType container,
KeYJavaType kjt,
PositionInfo pi,
Sort heapSort,
int heapCount) |
ProgramVariable(ProgramElementName name,
Sort s,
KeYJavaType t,
KeYJavaType containingType,
boolean isStatic,
boolean isModel,
boolean isGhost) |
ProgramVariable(ProgramElementName name,
Sort s,
KeYJavaType t,
KeYJavaType containingType,
boolean isStatic,
boolean isModel,
boolean isGhost,
boolean isFinal) |
Constructor and Description |
---|
ObserverFunction(java.lang.String baseName,
Sort sort,
KeYJavaType type,
Sort heapSort,
KeYJavaType container,
boolean isStatic,
ImmutableArray<KeYJavaType> paramTypes,
int heapCount,
int stateCount) |
Modifier and Type | Method and Description |
---|---|
KeYJavaType |
ProblemFinder.visitArrayopid(KeYParser.ArrayopidContext ctx) |
KeYJavaType |
DefaultBuilder.visitKeyjavatype(KeYParser.KeyjavatypeContext ctx) |
Modifier and Type | Field and Description |
---|---|
KeYJavaType |
ObserverWithType.kjt |
Constructor and Description |
---|
ObserverWithType(KeYJavaType kjt,
IObserverFunction obs) |
Modifier and Type | Method and Description |
---|---|
protected KeYJavaType |
ClassAxiomAndInvariantProofReferencesAnalyst.findProofsKeYJavaType(Services services)
Returns the
KeYJavaType which provides the proof obligation of the current proof. |
Modifier and Type | Method and Description |
---|---|
KeYJavaType |
FunctionalBlockContractPO.getCalleeKeYJavaType() |
KeYJavaType |
FunctionalLoopContractPO.getCalleeKeYJavaType() |
protected abstract KeYJavaType |
AbstractOperationPO.getCalleeKeYJavaType()
Returns the
KeYJavaType which contains AbstractOperationPO.getProgramMethod() . |
protected KeYJavaType |
FunctionalOperationContractPO.getCalleeKeYJavaType()
Returns the
KeYJavaType which contains AbstractOperationPO.getProgramMethod() . |
KeYJavaType |
DependencyContractPO.getContainerType()
Returns the
KeYJavaType in which the proven element is contained in. |
KeYJavaType |
KeYUserProblemFile.getContainerType()
Returns the
KeYJavaType in which the proven element is contained in. |
KeYJavaType |
WellDefinednessPO.getContainerType()
Returns the
KeYJavaType in which the proven element is contained in. |
KeYJavaType |
ProofOblInput.getContainerType()
Returns the
KeYJavaType in which the proven element is contained in. |
KeYJavaType |
FunctionalOperationContractPO.getContainerType()
Returns the
KeYJavaType in which the proven element is contained in. |
KeYJavaType |
AbstractPO.getContainerType()
Returns the
KeYJavaType in which the proven element is contained in. |
KeYJavaType |
WellDefinednessPO.getKJT() |
Modifier and Type | Method and Description |
---|---|
protected Term |
AbstractOperationPO.buildFreePre(ProgramVariable selfVar,
KeYJavaType selfKJT,
ImmutableList<ProgramVariable> paramVars,
java.util.List<LocationVariable> heaps,
Services services)
Builds the "general assumption".
|
protected void |
AbstractPO.collectClassAxioms(KeYJavaType selfKJT,
InitConfig proofConfig) |
protected Term |
AbstractPO.generateSelfExactType(IProgramMethod pm,
ProgramVariable selfVar,
KeYJavaType selfKJT)
Generates the general assumption which defines the type of self.
|
protected Term |
AbstractPO.generateSelfExactType(IProgramMethod pm,
Term selfVar,
KeYJavaType selfKJT)
Generates the general assumption which defines the type of self.
|
protected ImmutableSet<ClassAxiom> |
WellDefinednessPO.selectClassAxioms(KeYJavaType kjt) |
protected ImmutableSet<ClassAxiom> |
AbstractPO.selectClassAxioms(KeYJavaType selfKJT) |
Constructor and Description |
---|
ProofObligationVars(IProgramMethod pm,
KeYJavaType kjt,
Services services) |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<Pair<KeYJavaType,IObserverFunction>> |
SpecificationRepository.getOverridingTargets(KeYJavaType kjt,
IObserverFunction target) |
Modifier and Type | Method and Description |
---|---|
void |
SpecificationRepository.addRepresentsTermToWdChecksForModelFields(KeYJavaType kjt)
Represent terms belong to model fields, so the well-definedness check
considers both of them together.
|
boolean |
ProofCorrectnessMgt.contractApplicableFor(KeYJavaType kjt,
IObserverFunction target)
Deprecated.
|
ImmutableSet<ClassAxiom> |
SpecificationRepository.getClassAxioms(KeYJavaType selfKjt)
Returns all class axioms visible in the passed class, including the
axioms induced by invariant declarations.
|
ImmutableSet<ClassInvariant> |
SpecificationRepository.getClassInvariants(KeYJavaType kjt)
Returns all known class invariants for the passed type.
|
ImmutableSet<Contract> |
SpecificationRepository.getContracts(KeYJavaType kjt,
IObserverFunction target)
Returns all registered (atomic) contracts for the passed target.
|
ImmutableSet<IObserverFunction> |
SpecificationRepository.getContractTargets(KeYJavaType kjt)
Returns all functions for which contracts are registered in the passed
type.
|
ImmutableSet<FunctionalOperationContract> |
SpecificationRepository.getOperationContracts(KeYJavaType kjt,
IProgramMethod pm)
Returns all registered (atomic) operation contracts for the passed
operation.
|
ImmutableSet<FunctionalOperationContract> |
SpecificationRepository.getOperationContracts(KeYJavaType kjt,
IProgramMethod pm,
Modality modality)
Returns all registered (atomic) operation contracts for the passed
operation which refer to the passed modality.
|
ImmutableSet<Pair<KeYJavaType,IObserverFunction>> |
SpecificationRepository.getOverridingTargets(KeYJavaType kjt,
IObserverFunction target) |
ImmutableSet<Proof> |
SpecificationRepository.getProofs(KeYJavaType kjt,
IObserverFunction target)
Returns all proofs registered for the passed target and its overriding
targets.
|
Modifier and Type | Field and Description |
---|---|
KeYJavaType |
UseOperationContractRule.Instantiation.staticType
The static KeYJavaType.
|
Modifier and Type | Method and Description |
---|---|
KeYJavaType |
NewVarcond.getType() |
Modifier and Type | Method and Description |
---|---|
Term |
AuxiliaryContractBuilders.ConditionsAndClausesBuilder.buildSelfConditions(java.util.List<LocationVariable> heaps,
IProgramMethod pm,
KeYJavaType selfKJT,
Term self,
Services services)
Builds the assumptions for the
self variable
(self != null & self.created == true & exactInstance(self) ) |
protected static ProgramVariable |
AbstractAuxiliaryContractRule.createLocalVariable(java.lang.String nameBase,
KeYJavaType type,
Services services) |
static ImmutableSet<Contract> |
UseDependencyContractRule.getApplicableContracts(Services services,
KeYJavaType kjt,
IObserverFunction target)
Returns the dependency contracts which are applicable for the passed
target.
|
Constructor and Description |
---|
Instantiation(Term u,
Term progPost,
Modality mod,
Expression actualResult,
Term actualSelf,
KeYJavaType staticType,
MethodOrConstructorReference mr,
IProgramMethod pm,
ImmutableList<Term> actualParams,
boolean transaction)
Creates a new instantiation for the contract rule and the given variables.
|
NewVarcond(SchemaVariable sv,
KeYJavaType type) |
Modifier and Type | Field and Description |
---|---|
protected KeYJavaType |
MethodCall.staticPrefixType |
Modifier and Type | Method and Description |
---|---|
protected KeYJavaType |
InitArray.getElementType(NewArray p_creationExpression) |
KeYJavaType |
ProgramTransformer.getKeYJavaType() |
KeYJavaType |
ProgramTransformer.getKeYJavaType(Services javaServ,
ExecutionContext ec) |
KeYJavaType |
ProgramTransformer.getKeYJavaType(TermServices javaServ) |
KeYJavaType |
ReplaceWhileLoop.returnType() |
Modifier and Type | Method and Description |
---|---|
protected java.util.List<Statement> |
ConstructorCall.constructorCallSequence(New constructorReference,
KeYJavaType classType,
SVInstantiations svInst,
Services services)
returns a sequence of statements modelling the Java constructor call
semantics explicitly
|
protected Statement |
InitArray.createAssignment(ReferencePrefix p_array,
int p_index,
Expression p_initializer,
KeYJavaType p_elementType,
TypeReference p_baseType)
Convert one variable initializers to an assignment to the
appropriate array element (the initializer may itself be an
array initializer, in which case a valid creation expression is
created by inserting the new-operator)
|
protected IProgramMethod |
MethodCall.getMethod(KeYJavaType prefixType,
MethodReference mr,
Services services)
Returns the method.
|
Modifier and Type | Method and Description |
---|---|
protected Statement |
MethodCall.makeIfCascade(ImmutableList<KeYJavaType> imps,
Services services)
TODO
|
Modifier and Type | Method and Description |
---|---|
void |
TacletBuilder.addVarsNew(SchemaVariable v,
KeYJavaType type)
adds a new new variable to the variable conditions of
the Taclet: v is new and has the given type
|
Taclet |
TacletGenerator.generateAxiomTaclet(Name tacletName,
Term originalAxiom,
ImmutableList<ProgramVariable> programVars,
KeYJavaType kjt,
RuleSet ruleSet,
TermServices services)
Returns a no-find taclet to the passed axiom.
|
ImmutableSet<Taclet> |
TacletGenerator.generateContractAxiomTaclets(Name name,
Term originalPre,
Term originalPost,
Term originalMby,
KeYJavaType kjt,
IObserverFunction target,
java.util.List<? extends ProgramVariable> heaps,
ProgramVariable originalSelfVar,
ProgramVariable originalResultVar,
java.util.Map<LocationVariable,ProgramVariable> atPreVars,
ImmutableList<ProgramVariable> originalParamVars,
ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
boolean satisfiabilityGuard,
TermServices services) |
ImmutableSet<Taclet> |
TacletGenerator.generateFunctionalRepresentsTaclets(Name name,
Term originalPreTerm,
Term originalRepresentsTerm,
KeYJavaType kjt,
IObserverFunction target,
java.util.List<? extends ProgramVariable> heaps,
ProgramVariable self,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,ProgramVariable> atPreVars,
ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
boolean satisfiability,
Services services) |
ImmutableSet<Taclet> |
TacletGenerator.generatePartialInvTaclet(Name name,
java.util.List<SchemaVariable> heapSVs,
SchemaVariable selfSV,
SchemaVariable eqSV,
Term term,
KeYJavaType kjt,
ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
boolean isStatic,
boolean eqVersion,
Services services) |
Taclet |
TacletGenerator.generateRelationalRepresentsTaclet(Name tacletName,
Term originalAxiom,
KeYJavaType kjt,
IObserverFunction target,
java.util.List<? extends ProgramVariable> heaps,
ProgramVariable self,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,ProgramVariable> atPreVars,
boolean satisfiabilityGuard,
TermServices services) |
Constructor and Description |
---|
SMTObjTranslator(SMTSettings settings,
Services services,
KeYJavaType typeOfClassUnderTest) |
Modifier and Type | Method and Description |
---|---|
KeYJavaType |
PredicateAbstractionMergeContract.getKJT() |
KeYJavaType |
MethodWellDefinedness.getKJT() |
KeYJavaType |
AbstractAuxiliaryContractImpl.getKJT() |
KeYJavaType |
FunctionalAuxiliaryContract.getKJT() |
KeYJavaType |
ClassAxiomImpl.getKJT() |
KeYJavaType |
FunctionalOperationContractImpl.getKJT() |
KeYJavaType |
ClassWellDefinedness.getKJT() |
KeYJavaType |
ClassInvariantImpl.getKJT() |
KeYJavaType |
InformationFlowContractImpl.getKJT() |
KeYJavaType |
InitiallyClauseImpl.getKJT() |
KeYJavaType |
QueryAxiom.getKJT() |
KeYJavaType |
UnparameterizedMergeContract.getKJT() |
KeYJavaType |
PartialInvAxiom.getKJT() |
KeYJavaType |
ContractAxiom.getKJT() |
KeYJavaType |
LoopSpecification.getKJT() |
KeYJavaType |
DependencyContractImpl.getKJT() |
KeYJavaType |
RepresentsAxiom.getKJT() |
KeYJavaType |
LoopWellDefinedness.getKJT() |
KeYJavaType |
BlockWellDefinedness.getKJT() |
KeYJavaType |
SpecificationElement.getKJT()
Returns the KeYJavaType representing the class/interface to which the
specification element belongs.
|
KeYJavaType |
ModelMethodExecution.getKJT() |
KeYJavaType |
LoopSpecImpl.getKJT() |
KeYJavaType |
FunctionalOperationContractImpl.getSpecifiedIn() |
KeYJavaType |
InformationFlowContractImpl.getSpecifiedIn() |
KeYJavaType |
InformationFlowContract.getSpecifiedIn() |
KeYJavaType |
FunctionalOperationContract.getSpecifiedIn() |
Modifier and Type | Method and Description |
---|---|
LoopSpecification |
LoopSpecification.create(LoopStatement loop,
IProgramMethod pm,
KeYJavaType kjt,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres)
Create and return a new loop specification element from the existing one
where the arguments given are replaced.
|
LoopSpecification |
LoopSpecImpl.create(LoopStatement loop,
IProgramMethod pm,
KeYJavaType kjt,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres) |
InformationFlowContract |
ContractFactory.createInformationFlowContract(KeYJavaType forClass,
IProgramMethod pm,
KeYJavaType specifiedIn,
Modality modality,
Term requires,
Term requiresFree,
Term measuredBy,
Term modifies,
boolean hasMod,
ProgramVariableCollection progVars,
Term accessible,
ImmutableList<InfFlowSpec> infFlowSpecs,
boolean toBeSaved) |
DependencyContract |
ContractFactory.dep(KeYJavaType containerType,
IObserverFunction pm,
KeYJavaType specifiedIn,
java.util.Map<LocationVariable,Term> requires,
Term measuredBy,
java.util.Map<ProgramVariable,Term> accessibles,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Term globalDefs) |
DependencyContract |
ContractFactory.dep(KeYJavaType kjt,
LocationVariable targetHeap,
Triple<IObserverFunction,Term,Term> dep,
ProgramVariable selfVar) |
DependencyContract |
ContractFactory.dep(java.lang.String string,
KeYJavaType containerType,
IObserverFunction pm,
KeYJavaType specifiedIn,
java.util.Map<LocationVariable,Term> requires,
Term measuredBy,
java.util.Map<ProgramVariable,Term> accessibles,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,? extends ProgramVariable> atPreVars,
Term globalDefs) |
ImmutableSet<SpecificationElement> |
SpecExtractor.extractClassSpecs(KeYJavaType kjt)
Returns the class invariants for the passed type.
|
FunctionalOperationContract |
ContractFactory.func(java.lang.String baseName,
KeYJavaType kjt,
IProgramMethod pm,
Modality modality,
java.util.Map<LocationVariable,Term> pres,
java.util.Map<LocationVariable,Term> freePres,
Term mby,
java.util.Map<LocationVariable,Term> posts,
java.util.Map<LocationVariable,Term> freePosts,
java.util.Map<LocationVariable,Term> axioms,
java.util.Map<LocationVariable,Term> mods,
java.util.Map<ProgramVariable,Term> accs,
java.util.Map<LocationVariable,java.lang.Boolean> hasMod,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
java.util.Map<LocationVariable,LocationVariable> atPreVars,
boolean toBeSaved)
Creates a new functional operation contract.
|
static java.lang.String |
ContractFactory.generateContractName(java.lang.String baseName,
KeYJavaType forClass,
IObserverFunction target,
KeYJavaType specifiedIn,
int myId) |
static java.lang.String |
ContractFactory.generateContractTypeName(java.lang.String baseName,
KeYJavaType forClass,
IObserverFunction target,
KeYJavaType specifiedIn) |
static java.lang.String |
ContractFactory.generateDisplayName(java.lang.String baseName,
KeYJavaType forClass,
IObserverFunction target,
KeYJavaType specifiedIn,
int myId) |
ClassInvariant |
ClassInvariantImpl.setKJT(KeYJavaType newKjt) |
InitiallyClause |
InitiallyClauseImpl.setKJT(KeYJavaType newKjt) |
ClassInvariant |
ClassInvariant.setKJT(KeYJavaType kjt)
Returns another class invariant like this one, except that it refers to the
passed KeYJavaType.
|
InitiallyClause |
InitiallyClause.setKJT(KeYJavaType newKjt) |
RepresentsAxiom |
RepresentsAxiom.setKJT(KeYJavaType newKjt) |
MethodWellDefinedness |
MethodWellDefinedness.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
Contract |
FunctionalOperationContractImpl.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
ClassWellDefinedness |
ClassWellDefinedness.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
LoopContract |
LoopContract.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
InformationFlowContract |
InformationFlowContractImpl.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
Contract |
FunctionalBlockContract.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
InformationFlowContract |
InformationFlowContract.setTarget(KeYJavaType newKJT,
IObserverFunction newPM)
Return a new contract which equals this contract except that the
the KeYJavaType and ObserverFunction are set to the new values.
|
LoopSpecification |
LoopSpecification.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
Contract |
DependencyContractImpl.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
BlockContract |
BlockContractImpl.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
Contract |
Contract.setTarget(KeYJavaType newKJT,
IObserverFunction newPM)
Returns a contract which is identical to this contract except that the KeYJavaType and
IObserverFunction are set to the new values.
|
Contract |
LoopWellDefinedness.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
BlockContract |
BlockContract.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
LoopContract |
LoopContractImpl.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
Contract |
BlockWellDefinedness.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
Contract |
FunctionalLoopContract.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
AuxiliaryContract |
AuxiliaryContract.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
LoopSpecification |
LoopSpecImpl.setTarget(KeYJavaType newKJT,
IObserverFunction newPM) |
Constructor and Description |
---|
ClassAxiomImpl(java.lang.String name,
KeYJavaType kjt,
VisibilityModifier visibility,
Term rep,
ProgramVariable selfVar) |
ClassAxiomImpl(java.lang.String name,
java.lang.String displayName,
KeYJavaType kjt,
VisibilityModifier visibility,
Term rep,
ProgramVariable selfVar) |
ClassInvariantImpl(java.lang.String name,
java.lang.String displayName,
KeYJavaType kjt,
VisibilityModifier visibility,
Term inv,
ParsableVariable selfVar)
Creates a class invariant.
|
ContractAxiom(java.lang.String name,
IObserverFunction target,
KeYJavaType kjt,
VisibilityModifier visibility,
Term pre,
Term post,
Term mby,
java.util.Map<LocationVariable,ProgramVariable> atPreVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
ImmutableList<ProgramVariable> paramVars) |
ContractAxiom(java.lang.String name,
java.lang.String displayName,
IObserverFunction target,
KeYJavaType kjt,
VisibilityModifier visibility,
Term originalPre,
Term originalPost,
Term originalMby,
java.util.Map<LocationVariable,ProgramVariable> atPreVars,
ProgramVariable selfVar,
ProgramVariable resultVar,
ImmutableList<ProgramVariable> paramVars) |
InformationFlowContractImpl(java.lang.String baseName,
KeYJavaType forClass,
IProgramMethod pm,
KeYJavaType specifiedIn,
Modality modality,
Term pre,
Term freePre,
Term mby,
Term mod,
boolean hasRealMod,
Term self,
ImmutableList<Term> params,
Term result,
Term exc,
Term heapAtPre,
Term dep,
ImmutableList<InfFlowSpec> infFlowSpecs,
boolean toBeSaved) |
InformationFlowContractImpl(java.lang.String baseName,
java.lang.String name,
KeYJavaType forClass,
IProgramMethod pm,
KeYJavaType specifiedIn,
Modality modality,
Term pre,
Term freePre,
Term mby,
Term mod,
boolean hasRealMod,
Term self,
ImmutableList<Term> params,
Term result,
Term exc,
Term heapAtPre,
Term dep,
ImmutableList<InfFlowSpec> infFlowSpecs,
boolean toBeSaved,
int id) |
InitiallyClauseImpl(java.lang.String name,
java.lang.String displayName,
KeYJavaType kjt,
VisibilityModifier visibility,
Term inv,
ParsableVariable selfVar,
LabeledParserRuleContext originalSpec)
Creates a class invariant.
|
LoopSpecImpl(LoopStatement loop,
IProgramMethod pm,
KeYJavaType kjt,
java.util.Map<LocationVariable,Term> invariants,
java.util.Map<LocationVariable,Term> freeInvariants,
java.util.Map<LocationVariable,Term> modifies,
java.util.Map<LocationVariable,ImmutableList<InfFlowSpec>> infFlowSpecs,
Term variant,
Term selfTerm,
ImmutableList<Term> localIns,
ImmutableList<Term> localOuts,
java.util.Map<LocationVariable,Term> atPres)
Creates a loop invariant.
|
LoopSpecImpl(LoopStatement loop,
IProgramMethod pm,
KeYJavaType kjt,
Term selfTerm,
java.util.Map<LocationVariable,Term> atPres)
Creates an empty, default loop invariant for the passed loop.
|
ModelMethodExecution(java.lang.String name,
IObserverFunction target,
KeYJavaType kjt,
VisibilityModifier visibility) |
ModelMethodExecution(java.lang.String name,
java.lang.String displayName,
IObserverFunction target,
KeYJavaType kjt,
VisibilityModifier visibility) |
PredicateAbstractionMergeContract(MergePointStatement mps,
java.util.Map<LocationVariable,Term> atPres,
KeYJavaType kjt,
java.lang.String latticeType,
java.util.List<AbstractionPredicate> abstractionPredicates) |
QueryAxiom(java.lang.String name,
IProgramMethod target,
KeYJavaType kjt) |
RepresentsAxiom(java.lang.String name,
IObserverFunction target,
KeYJavaType kjt,
VisibilityModifier visibility,
Term pre,
Term rep,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,ProgramVariable> atPreVars) |
RepresentsAxiom(java.lang.String name,
java.lang.String displayName,
IObserverFunction target,
KeYJavaType kjt,
VisibilityModifier visibility,
Term pre,
Term rep,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,ProgramVariable> atPreVars) |
UnparameterizedMergeContract(MergeProcedure mergeProcedure,
MergePointStatement mps,
KeYJavaType kjt) |
Modifier and Type | Method and Description |
---|---|
static ImmutableSet<LabeledParserRuleContext> |
JMLSpecExtractor.createNonNullPositionedString(java.lang.String varName,
KeYJavaType kjt,
boolean isImplicitVar,
java.lang.String fileName,
Position pos,
Services services)
creates a JML specification expressing that the given variable/field is
not null and in case of a reference array type that also its elements are
non-null In case of implicit fields or primitive typed fields/variables
the empty set is returned
|
ImmutableSet<SpecificationElement> |
JMLSpecExtractor.extractClassSpecs(KeYJavaType kjt) |
static boolean |
JMLInfoExtractor.isNullable(java.lang.String fieldName,
KeYJavaType containingClass)
Returns true, if containingClass is a reference Type and has a
field declaration with name fieldName, which is explicitly or
implicitly declared "nullable"
|
static boolean |
JMLInfoExtractor.isNullableByDefault(KeYJavaType t)
Returns true if the given type is specified as nullable, i.e.
|
static boolean |
JMLInfoExtractor.isPureByDefault(KeYJavaType t)
Returns true iff the given type is specified as pure, i.e.
|
static boolean |
JMLInfoExtractor.isStrictlyPureByDefault(KeYJavaType t)
Returns true iff the given type is specified as pure, i.e.
|
Constructor and Description |
---|
JMLBuiltInPropertyResolver(JavaInfo javaInfo,
SLResolverManager manager,
KeYJavaType specInClass) |
JMLResolverManager(JavaInfo javaInfo,
KeYJavaType specInClass,
ParsableVariable selfVar,
SLExceptionFactory eManager) |
Modifier and Type | Field and Description |
---|---|
protected KeYJavaType |
JmlTermFactory.bigint |
Modifier and Type | Method and Description |
---|---|
SLExpression |
JmlTermFactory.bsum(SLExpression a,
SLExpression b,
SLExpression t,
KeYJavaType declsType,
ImmutableList<LogicVariable> declVars) |
SLExpression |
JmlTermFactory.cast(KeYJavaType type,
SLExpression result) |
JmlIO |
JmlIO.classType(KeYJavaType classType)
Sets the sort/type of the class containing the interpreted JML.
|
SLExpression |
JmlTermFactory.createInv(Term selfVar,
KeYJavaType targetType)
Need to handle this one differently from INV_FOR
since here also static invariants may occur.
|
SLExpression |
JmlTermFactory.createSeqDef(SLExpression a,
SLExpression b,
SLExpression t,
KeYJavaType declsType,
ImmutableList<? extends QuantifiableVariable> declVars) |
SLExpression |
JmlTermFactory.exists(Term preTerm,
Term bodyTerm,
KeYJavaType declsType,
ImmutableList<LogicVariable> declVars,
boolean nullable,
KeYJavaType resultType) |
SLExpression |
JmlTermFactory.forall(Term preTerm,
Term bodyTerm,
KeYJavaType declsType,
ImmutableList<LogicVariable> declVars,
boolean nullable,
KeYJavaType resultType) |
SLExpression |
JmlTermFactory.quantifiedMax(Term _guard,
Term body,
KeYJavaType declsType,
boolean nullable,
ImmutableList<LogicVariable> qvs) |
SLExpression |
JmlTermFactory.quantifiedMin(Term _guard,
Term body,
KeYJavaType declsType,
boolean nullable,
ImmutableList<LogicVariable> qvs) |
SLExpression |
JmlTermFactory.quantifiedNumOf(Term t1,
Term t2,
KeYJavaType declsType,
boolean nullable,
java.lang.Iterable<LogicVariable> qvs,
KeYJavaType resultType) |
SLExpression |
JmlTermFactory.quantifiedProduct(KeYJavaType declsType,
boolean nullable,
java.lang.Iterable<LogicVariable> qvs,
Term t1,
Term t2,
KeYJavaType resultType) |
SLExpression |
JmlTermFactory.quantifiedSum(KeYJavaType javaType,
boolean nullable,
java.lang.Iterable<LogicVariable> qvs,
Term t1,
Term t2,
KeYJavaType resultType) |
Term |
JmlTermFactory.signals(Term result,
LogicVariable eVar,
ProgramVariable excVar,
KeYJavaType excType) |
SLExpression |
JmlTermFactory.skolemExprHelper(KeYJavaType type,
TermServices services,
java.lang.String shortName) |
SLExpression |
JmlTermFactory.skolemExprHelper(java.lang.String jmlKeyWord,
KeYJavaType type,
TermServices services) |
SLExpression |
JmlTermFactory.skolemExprHelper(org.antlr.runtime.Token jmlKeyWord,
KeYJavaType type,
TermServices services) |
SLExpression |
JmlTermFactory.staticInfFor(KeYJavaType kjt) |
protected Term |
JmlTermFactory.typerestrict(KeYJavaType kjt,
boolean nullable,
java.lang.Iterable<? extends QuantifiableVariable> qvs)
Provide restriction terms for the declared KeYJavaType
Note that these restrictions only apply to the JML to DL translation.
|
SLExpression |
JmlTermFactory.values(KeYJavaType t) |
Modifier and Type | Method and Description |
---|---|
SLExpression |
JmlTermFactory.createUnionF(boolean nullable,
Pair<KeYJavaType,ImmutableList<LogicVariable>> declVars,
Term expr,
Term guard) |
Term |
JmlTermFactory.signalsOnly(ImmutableList<KeYJavaType> signalsonly,
ProgramVariable excVar) |
Constructor and Description |
---|
JmlIO(Services services,
KeYJavaType specInClass,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
java.util.Map<LocationVariable,Term> atPres,
java.util.Map<LocationVariable,Term> atBefores)
Full constructor of this class.
|
Modifier and Type | Field and Description |
---|---|
protected KeYJavaType |
SLExpressionResolver.specInClass |
Modifier and Type | Method and Description |
---|---|
KeYJavaType |
SLExpression.getType() |
Modifier and Type | Method and Description |
---|---|
ImmutableList<KeYJavaType> |
SLParameters.getSignature(Services services)
returns the type signature of the parameter list
|
Modifier and Type | Method and Description |
---|---|
SLExpression |
JavaIntegerSemanticsHelper.buildCastExpression(KeYJavaType resultType,
SLExpression a) |
protected boolean |
SLExpressionResolver.isVisible(MemberDeclaration md,
KeYJavaType containingType)
Checks whether the passed member, contained in the passed type,
is visible in specInClass.
|
void |
SLResolverManager.putIntoTopLocalVariablesNamespace(ImmutableList<LogicVariable> pvs,
KeYJavaType kjt)
Puts a list of local variables into the topmost namespace on the stack.
|
void |
SLResolverManager.putIntoTopLocalVariablesNamespace(ParsableVariable pv,
KeYJavaType kjt)
Puts a local variable into the topmost namespace on the stack
|
Constructor and Description |
---|
SLAttributeResolver(JavaInfo javaInfo,
SLResolverManager manager,
KeYJavaType specInClass) |
SLExpression(KeYJavaType type) |
SLExpression(Term term,
KeYJavaType type) |
SLExpression(Term term,
KeYJavaType type,
boolean isTerm) |
SLExpressionResolver(JavaInfo javaInfo,
SLResolverManager manager,
KeYJavaType specInClass) |
SLMethodResolver(JavaInfo javaInfo,
SLResolverManager manager,
KeYJavaType specInClass) |
SLResolverManager(SLExceptionFactory excManager,
KeYJavaType specInClass,
ParsableVariable selfVar,
boolean useLocalVarsAsImplicitReceivers,
TermBuilder tb) |
SLTypeResolver(JavaInfo javaInfo,
SLResolverManager manager,
KeYJavaType specInClass) |
Modifier and Type | Method and Description |
---|---|
protected Term |
ExecutionOperationContract.searchConstructorSelfDefinition(Term term,
KeYJavaType staticType,
Services services)
Tries to find the self
Term of the given KeYJavaType . |
Modifier and Type | Method and Description |
---|---|
protected KeYJavaType |
ProgramMethodPO.getCalleeKeYJavaType()
Returns the
KeYJavaType which contains AbstractOperationPO.getProgramMethod() . |
KeYJavaType |
ProgramMethodPO.getContainerType()
Returns the
KeYJavaType in which the proven element is contained in. |
Modifier and Type | Method and Description |
---|---|
protected Term |
ProgramMethodSubsetPO.buildFreePre(ProgramVariable selfVar,
KeYJavaType selfKJT,
ImmutableList<ProgramVariable> paramVars,
java.util.List<LocationVariable> heaps,
Services proofServices)
Builds the "general assumption".
|
Constructor and Description |
---|
AbstractConditionalBreakpoint(int hitCount,
IProgramMethod pm,
Proof proof,
boolean enabled,
boolean conditionEnabled,
int methodStart,
int methodEnd,
KeYJavaType containerType)
Creates a new
AbstractConditionalBreakpoint . |
FieldWatchpoint(boolean enabled,
int hitCount,
java.lang.String fieldName,
boolean isAcces,
boolean isModification,
KeYJavaType containerKJT,
Proof proof)
Creates a new
FieldWatchpoint . |
KeYWatchpoint(int hitCount,
Proof proof,
java.lang.String condition,
boolean enabled,
boolean conditionEnabled,
KeYJavaType containerType,
boolean suspendOnTrue)
Creates a new
AbstractConditionalBreakpoint . |
Modifier and Type | Method and Description |
---|---|
KeYJavaType |
TacletProofObligationInput.getContainerType()
Returns the
KeYJavaType in which the proven element is contained in. |
Modifier and Type | Method and Description |
---|---|
KeYJavaType |
ProofInfo.getReturnType() |
KeYJavaType |
ProofInfo.getTypeOfClassUnderTest() |
Modifier and Type | Method and Description |
---|---|
KeYJavaType |
ProofStarter.UserProvidedInput.getContainerType()
Returns the
KeYJavaType in which the proven element is contained in. |
static KeYJavaType |
KeYTypeUtil.getType(Services services,
java.lang.String fullName)
Returns the
KeYJavaType fore the given name. |
Modifier and Type | Method and Description |
---|---|
static java.lang.String |
KeYTypeUtil.getParentName(Services services,
KeYJavaType type)
Returns the name of the parent package/type or
null if it has no one. |
static boolean |
KeYTypeUtil.isInnerType(Services services,
KeYJavaType type)
Checks if the given type is an inner or anonymous type.
|
static boolean |
KeYTypeUtil.isLibraryClass(KeYJavaType kjt)
Checks if the given
KeYJavaType is a library class. |
Copyright © 2003-2019 The KeY-Project.