Package | Description |
---|---|
de.uka.ilkd.key.control | |
de.uka.ilkd.key.core | |
de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
|
de.uka.ilkd.key.nparser.builder | |
de.uka.ilkd.key.parser |
This package contains the parser for .key and .proof files.
|
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.init |
This package contains classes handling prover initialisation.
|
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 |
Modifier and Type | Method and Description |
---|---|
JavaInfo |
KeYEnvironment.getJavaInfo()
Returns the used
JavaInfo . |
Modifier and Type | Method and Description |
---|---|
JavaInfo |
KeYMediator.getJavaInfo()
returns the JavaInfo with the java type information
|
Modifier and Type | Method and Description |
---|---|
JavaInfo |
JavaInfo.copy(Services serv)
copies this JavaInfo and uses the given Services object as the
Services object of the copied JavaInfo
|
JavaInfo |
Services.getJavaInfo()
Returns the JavaInfo associated with this Services object.
|
Modifier and Type | Method and Description |
---|---|
static FieldReference |
KeYJavaASTFactory.arrayLength(JavaInfo model,
ReferencePrefix array)
Create an array length access.
|
static Catch |
KeYJavaASTFactory.catchClause(JavaInfo javaInfo,
java.lang.String param,
KeYJavaType kjt,
StatementBlock body)
Create a catch clause.
|
static Catch |
KeYJavaASTFactory.catchClause(JavaInfo javaInfo,
java.lang.String param,
java.lang.String type,
StatementBlock body)
Create a catch clause.
|
static IGuard |
KeYJavaASTFactory.lessThanArrayLengthGuard(JavaInfo model,
ProgramVariable variable,
ReferencePrefix array)
Create a condition that compares a variable and an array length using the
less than operator.
|
static MethodBodyStatement |
KeYJavaASTFactory.methodBody(JavaInfo model,
ProgramVariable result,
ReferencePrefix reference,
KeYJavaType classType,
java.lang.String methodName,
ProgramVariable[] arguments)
Create a method body shortcut.
|
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
|
static ParameterDeclaration |
KeYJavaASTFactory.parameterDeclaration(JavaInfo javaInfo,
java.lang.String type,
java.lang.String name) |
Constructor and Description |
---|
JavaInfo(JavaInfo proto,
Services s) |
Modifier and Type | Method and Description |
---|---|
JavaInfo |
DefaultBuilder.getJavaInfo() |
Modifier and Type | Method and Description |
---|---|
JavaInfo |
ParserConfig.javaInfo() |
Modifier and Type | Method and Description |
---|---|
JavaInfo |
Proof.getJavaInfo()
returns the JavaInfo with the java type information
|
Modifier and Type | Field and Description |
---|---|
protected JavaInfo |
AbstractPO.javaInfo |
Constructor and Description |
---|
JMLBuiltInPropertyResolver(JavaInfo javaInfo,
SLResolverManager manager,
KeYJavaType specInClass) |
JMLResolverManager(JavaInfo javaInfo,
KeYJavaType specInClass,
ParsableVariable selfVar,
SLExceptionFactory eManager) |
Modifier and Type | Method and Description |
---|---|
SLExpression |
JmlTermFactory.createIntersect(Term t,
JavaInfo javaInfo) |
SLExpression |
JmlTermFactory.createUnion(JavaInfo javaInfo,
Term t) |
SLExpression |
JmlTermFactory.empty(JavaInfo javaInfo) |
Modifier and Type | Field and Description |
---|---|
protected JavaInfo |
SLExpressionResolver.javaInfo |
Constructor and Description |
---|
SLAttributeResolver(JavaInfo javaInfo,
SLResolverManager manager,
KeYJavaType specInClass) |
SLExpressionResolver(JavaInfo javaInfo,
SLResolverManager manager,
KeYJavaType specInClass) |
SLMethodResolver(JavaInfo javaInfo,
SLResolverManager manager,
KeYJavaType specInClass) |
SLTypeResolver(JavaInfo javaInfo,
SLResolverManager manager,
KeYJavaType specInClass) |
Copyright © 2003-2019 The KeY-Project.