public final class JMLTranslator
extends java.lang.Object
Modifier and Type | Class and Description |
---|---|
private class |
JMLTranslator.JMLArithmeticOperationTranslationMethod
Translation methods for (binary) arithmetic operations.
|
private class |
JMLTranslator.JMLBoundedNumericalQuantifierTranslationMethod |
private class |
JMLTranslator.JMLEqualityTranslationMethod |
private class |
JMLTranslator.JMLFieldAccessExpressionTranslationMethod
Abstract super-class for translation methods which enumerate fields such as
\reach . |
static class |
JMLTranslator.JMLKeyWord |
private class |
JMLTranslator.JMLQuantifierTranslationMethod |
Modifier and Type | Field and Description |
---|---|
private SLTranslationExceptionManager |
excManager |
private java.lang.String |
fileName |
static java.util.Map<java.lang.String,java.lang.String> |
jml2jdl |
private TermServices |
services |
private TermBuilder |
tb |
private java.util.EnumMap<JMLTranslator.JMLKeyWord,JMLTranslationMethod> |
translationMethods |
private java.util.List<PositionedString> |
warnings |
Constructor and Description |
---|
JMLTranslator(SLTranslationExceptionManager excManager,
java.lang.String fileName,
TermServices services) |
JMLTranslator(SLTranslationExceptionManager excManager,
TermServices services) |
Modifier and Type | Method and Description |
---|---|
(package private) void |
addDeprecatedWarning(java.lang.String feature) |
(package private) void |
addIgnoreWarning(java.lang.String feature)
This is used for features without semantics such as labels or annotations.
|
(package private) void |
addIgnoreWarning(java.lang.String feature,
org.antlr.runtime.Token t) |
private void |
addUnderspecifiedWarning(java.lang.String feature)
Used for features with semantics (currently) not supported in KeY/DL.
|
private void |
addUnderspecifiedWarning(org.antlr.runtime.Token t) |
private void |
addWarning(java.lang.String msg) |
private void |
addWarning(java.lang.String msg,
org.antlr.runtime.Token t) |
private static <T> T |
castToReturnType(java.lang.Object result,
java.lang.Class<T> resultClass) |
private void |
checkParameters(java.lang.Object[] params,
java.lang.Class<?>... classes) |
(package private) SLExpression |
createSkolemExprBigint(org.antlr.runtime.Token jmlKeyWord,
Services services)
Create a skolem term (wrapped in SLExpression) for currently unsupported JML expressions of type \bigint.
|
(package private) SLExpression |
createSkolemExprBool(org.antlr.runtime.Token jmlKeyWord)
Create a nullary predicate (wrapped in SLExpression) for currently unsupported JML expressions of type boolean.
|
(package private) SLExpression |
createSkolemExprInt(org.antlr.runtime.Token jmlKeyWord,
Services services)
Create a skolem term (wrapped in SLExpression) for currently unsupported JML expressions of type int.
|
(package private) SLExpression |
createSkolemExprLong(org.antlr.runtime.Token jmlKeyWord,
Services services)
Create a skolem term (wrapped in SLExpression) for currently unsupported JML expressions of type long.
|
(package private) SLExpression |
createSkolemExprObject(org.antlr.runtime.Token jmlKeyWord,
Services services)
Create a skolem term (wrapped in SLExpression) for currently unsupported JML expressions of type Object.
|
java.util.List<PositionedString> |
getWarnings()
Get non-critical warnings.
|
java.lang.String |
getWarningsAsString()
Get non-critical warnings.
|
private SLExpression |
skolemExprHelper(org.antlr.runtime.Token jmlKeyWord,
KeYJavaType type,
TermServices services) |
private SLExpression |
skolemExprHelper(org.antlr.runtime.Token jmlKeyWord,
PrimitiveType type,
Services services) |
(package private) <T> T |
translate(JMLTranslator.JMLKeyWord keyword,
java.lang.Class<T> resultClass,
java.lang.Object... params) |
(package private) SLExpression |
translate(JMLTranslator.JMLKeyWord keyword,
java.lang.Object... params) |
static <T> T |
translate(PositionedString expr,
KeYJavaType specInClass,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
java.util.Map<LocationVariable,Term> atPres,
java.lang.Class<T> resultClass,
Services services) |
static <T> T |
translate(PositionedString expr,
KeYJavaType specInClass,
ProgramVariable selfVar,
ImmutableList<ProgramVariable> paramVars,
ProgramVariable resultVar,
ProgramVariable excVar,
java.util.Map<LocationVariable,Term> atPres,
java.util.Map<LocationVariable,Term> atBefores,
java.lang.Class<T> resultClass,
Services services) |
(package private) <T> T |
translate(java.lang.String jmlKeyWordName,
java.lang.Class<T> resultClass,
java.lang.Object... params) |
(package private) static <T> T |
translate(java.lang.String jmlExpr,
KeYJavaType specInClass,
java.lang.Class<T> resultClass,
Services services)
For testing only.
|
(package private) SLExpression |
translate(java.lang.String jmlKeyWordName,
java.lang.Object... params) |
SLExpression |
translateMapExpressionToJDL(org.antlr.runtime.Token t,
ImmutableList<SLExpression> list,
Services services) |
private static SLExpression |
translateToJDLTerm(org.antlr.runtime.Token escape,
java.lang.String functName,
Services services,
TermBuilder tb,
ImmutableList<SLExpression> list,
SLTranslationExceptionManager excManager) |
protected Term |
typerestrict(KeYJavaType kjt,
boolean nullable,
java.lang.Iterable<? extends QuantifiableVariable> qvs,
Services services)
Provide restriction terms for the declared KeYJavaType
Note that these restrictions only apply to the JML to DL translation.
|
private final TermBuilder tb
private final java.lang.String fileName
private TermServices services
private SLTranslationExceptionManager excManager
private java.util.List<PositionedString> warnings
private java.util.EnumMap<JMLTranslator.JMLKeyWord,JMLTranslationMethod> translationMethods
public static final java.util.Map<java.lang.String,java.lang.String> jml2jdl
public JMLTranslator(SLTranslationExceptionManager excManager, TermServices services)
public JMLTranslator(SLTranslationExceptionManager excManager, java.lang.String fileName, TermServices services)
public static <T> T translate(PositionedString expr, KeYJavaType specInClass, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar, ProgramVariable excVar, java.util.Map<LocationVariable,Term> atPres, java.lang.Class<T> resultClass, Services services) throws SLTranslationException
SLTranslationException
public static <T> T translate(PositionedString expr, KeYJavaType specInClass, ProgramVariable selfVar, ImmutableList<ProgramVariable> paramVars, ProgramVariable resultVar, ProgramVariable excVar, java.util.Map<LocationVariable,Term> atPres, java.util.Map<LocationVariable,Term> atBefores, java.lang.Class<T> resultClass, Services services) throws SLTranslationException
SLTranslationException
static <T> T translate(java.lang.String jmlExpr, KeYJavaType specInClass, java.lang.Class<T> resultClass, Services services) throws SLTranslationException
SLTranslationException
<T> T translate(java.lang.String jmlKeyWordName, java.lang.Class<T> resultClass, java.lang.Object... params) throws SLTranslationException
SLTranslationException
<T> T translate(JMLTranslator.JMLKeyWord keyword, java.lang.Class<T> resultClass, java.lang.Object... params) throws SLTranslationException
SLTranslationException
SLExpression translate(java.lang.String jmlKeyWordName, java.lang.Object... params) throws SLTranslationException
SLTranslationException
SLExpression translate(JMLTranslator.JMLKeyWord keyword, java.lang.Object... params) throws SLTranslationException
SLTranslationException
SLExpression createSkolemExprInt(org.antlr.runtime.Token jmlKeyWord, Services services)
SLExpression createSkolemExprLong(org.antlr.runtime.Token jmlKeyWord, Services services)
SLExpression createSkolemExprBigint(org.antlr.runtime.Token jmlKeyWord, Services services)
SLExpression createSkolemExprObject(org.antlr.runtime.Token jmlKeyWord, Services services)
SLExpression createSkolemExprBool(org.antlr.runtime.Token jmlKeyWord)
public java.util.List<PositionedString> getWarnings()
public java.lang.String getWarningsAsString()
private void checkParameters(java.lang.Object[] params, java.lang.Class<?>... classes) throws SLTranslationException
SLTranslationException
private static <T> T castToReturnType(java.lang.Object result, java.lang.Class<T> resultClass) throws SLTranslationException
SLTranslationException
private SLExpression skolemExprHelper(org.antlr.runtime.Token jmlKeyWord, PrimitiveType type, Services services)
private SLExpression skolemExprHelper(org.antlr.runtime.Token jmlKeyWord, KeYJavaType type, TermServices services)
void addIgnoreWarning(java.lang.String feature)
void addIgnoreWarning(java.lang.String feature, org.antlr.runtime.Token t)
private void addUnderspecifiedWarning(java.lang.String feature)
feature
- private void addUnderspecifiedWarning(org.antlr.runtime.Token t)
void addDeprecatedWarning(java.lang.String feature)
private void addWarning(java.lang.String msg)
private void addWarning(java.lang.String msg, org.antlr.runtime.Token t)
private static SLExpression translateToJDLTerm(org.antlr.runtime.Token escape, java.lang.String functName, Services services, TermBuilder tb, ImmutableList<SLExpression> list, SLTranslationExceptionManager excManager) throws SLTranslationException
SLTranslationException
public SLExpression translateMapExpressionToJDL(org.antlr.runtime.Token t, ImmutableList<SLExpression> list, Services services) throws SLTranslationException
SLTranslationException
protected Term typerestrict(KeYJavaType kjt, boolean nullable, java.lang.Iterable<? extends QuantifiableVariable> qvs, Services services)
TermBuilder.reachableValue(Term, KeYJavaType)
.