All Methods Instance Methods Concrete Methods
Modifier and Type |
Method and Description |
Term |
accessible(Term ensuresTerm) |
SLExpression |
add(SLExpression left,
SLExpression right) |
SLExpression |
antivalence(SLExpression left,
SLExpression right) |
SLExpression |
arrayRef(SLExpression receiver,
java.lang.String fullyQualifiedName,
SLExpression rangeFrom,
SLExpression rangeTo) |
Term |
assignable(Term term) |
SLExpression |
bsum(SLExpression a,
SLExpression b,
SLExpression t,
KeYJavaType declsType,
ImmutableList<LogicVariable> declVars) |
SLExpression |
cast(KeYJavaType type,
SLExpression result) |
protected void |
checkNotBigint(SLExpression e) |
void |
checkNotType(SLExpression e,
SLExceptionFactory man) |
protected void |
checkSLExpressions(SLExpression left,
SLExpression right,
java.lang.String eqSymb) |
SLExpression |
commentary(java.lang.String desc,
ProgramVariable selfVar,
ProgramVariable resultVar,
ImmutableList<ProgramVariable> paramVars,
Term heapAtPre) |
Pair<Label,Term> |
createBreaks(Term term,
java.lang.String label) |
Pair<Label,Term> |
createContinues(Term term,
java.lang.String label) |
SLExpression |
createIndexOf(Term seq,
Term elem) |
SLExpression |
createIntersect(Term t,
JavaInfo javaInfo) |
SLExpression |
createInv(Term selfVar,
KeYJavaType targetType)
Need to handle this one differently from INV_FOR
since here also static invariants may occur.
|
Term |
createLocSet(ImmutableList<SLExpression> exprList) |
SLExpression |
createPairwiseDisjoint(ImmutableList<Term> list) |
Term |
createReturns(Term term) |
SLExpression |
createSeqDef(SLExpression a,
SLExpression b,
SLExpression t,
KeYJavaType declsType,
ImmutableList<? extends QuantifiableVariable> declVars) |
SLExpression |
createSkolemExprBool(java.lang.String jmlKeyWord) |
SLExpression |
createSkolemExprBool(org.antlr.runtime.Token jmlKeyWord)
Create a nullary predicate (wrapped in SLExpression) for currently unsupported JML expressions of type boolean.
|
SLExpression |
createSkolemExprLong(java.lang.String text) |
SLExpression |
createSkolemExprObject(java.lang.String jmlKeyWord) |
Term |
createStoreRef(SLExpression expr) |
SLExpression |
createUnion(JavaInfo javaInfo,
Term t) |
SLExpression |
createUnionF(boolean nullable,
Pair<KeYJavaType,ImmutableList<LogicVariable>> declVars,
Term expr,
Term guard) |
Triple<IObserverFunction,Term,Term> |
depends(SLExpression lhs,
Term rhs,
SLExpression mby) |
SLExpression |
dlKeyword(java.lang.String name,
ImmutableList<SLExpression> list) |
SLExpression |
empty(JavaInfo javaInfo) |
SLExpression |
eq(SLExpression left,
SLExpression right) |
SLExpression |
equivalence(SLExpression left,
SLExpression right) |
SLExpression |
exists(Term preTerm,
Term bodyTerm,
KeYJavaType declsType,
ImmutableList<LogicVariable> declVars,
boolean nullable,
KeYJavaType resultType) |
SLExpression |
forall(Term preTerm,
Term bodyTerm,
KeYJavaType declsType,
ImmutableList<LogicVariable> declVars,
boolean nullable,
KeYJavaType resultType) |
SLExpression |
fresh(ImmutableList<SLExpression> list,
java.util.Map<LocationVariable,Term> atPres) |
java.util.List<PositionedString> |
getWarnings()
Get non-critical warnings.
|
java.lang.String |
getWarningsAsString()
Get non-critical warnings.
|
SLExpression |
index() |
ImmutableList<Term> |
infflowspeclist(ImmutableList<Term> result) |
SLExpression |
invFor(SLExpression param) |
protected boolean |
isBigint(SLExpression e) |
SLExpression |
ite(SLExpression result,
SLExpression a,
SLExpression b) |
SLExpression |
neq(SLExpression left,
SLExpression right) |
Term |
notModified(Term term,
SLExpression t) |
SLExpression |
quantifiedMax(Term _guard,
Term body,
KeYJavaType declsType,
boolean nullable,
ImmutableList<LogicVariable> qvs) |
SLExpression |
quantifiedMin(Term _guard,
Term body,
KeYJavaType declsType,
boolean nullable,
ImmutableList<LogicVariable> qvs) |
SLExpression |
quantifiedNumOf(Term t1,
Term t2,
KeYJavaType declsType,
boolean nullable,
java.lang.Iterable<LogicVariable> qvs,
KeYJavaType resultType) |
SLExpression |
quantifiedProduct(KeYJavaType declsType,
boolean nullable,
java.lang.Iterable<LogicVariable> qvs,
Term t1,
Term t2,
KeYJavaType resultType) |
SLExpression |
quantifiedSum(KeYJavaType javaType,
boolean nullable,
java.lang.Iterable<LogicVariable> qvs,
Term t1,
Term t2,
KeYJavaType resultType) |
SLExpression |
reach(Term t,
SLExpression e1,
SLExpression e2,
SLExpression e3) |
SLExpression |
reachLocs(Term t,
SLExpression e1,
SLExpression e2,
SLExpression e3) |
Pair<IObserverFunction,Term> |
represents(SLExpression lhs,
Term t) |
SLExpression |
seqConcat(Term seq1,
Term seq2) |
SLExpression |
seqConst(ImmutableList<SLExpression> exprList) |
SLExpression |
seqGet(Term seq,
Term idx) |
SLExpression |
shiftLeft(SLExpression result,
SLExpression e) |
SLExpression |
shiftRight(SLExpression a,
SLExpression e) |
Term |
signals(Term result,
LogicVariable eVar,
ProgramVariable excVar,
KeYJavaType excType) |
Term |
signalsOnly(ImmutableList<KeYJavaType> signalsonly,
ProgramVariable excVar) |
SLExpression |
skolemExprHelper(KeYJavaType type,
TermServices services,
java.lang.String shortName) |
SLExpression |
skolemExprHelper(java.lang.String jmlKeyWord,
KeYJavaType type,
TermServices services) |
SLExpression |
skolemExprHelper(java.lang.String jmlKeyWord,
PrimitiveType type) |
SLExpression |
skolemExprHelper(org.antlr.runtime.Token jmlKeyWord,
KeYJavaType type,
TermServices services) |
SLExpression |
skolemExprHelper(org.antlr.runtime.Token jmlKeyWord,
PrimitiveType type) |
SLExpression |
staticInfFor(KeYJavaType kjt) |
SLExpression |
substract(SLExpression left,
SLExpression right) |
SLExpression |
translateArrayReference(SLExpression receiver,
SLExpression rangeFrom,
SLExpression rangeTo) |
SLExpression |
translateMapExpressionToJDL(java.lang.String text,
ImmutableList<SLExpression> list,
Services services) |
SLExpression |
translateMapExpressionToJDL(org.antlr.runtime.Token t,
ImmutableList<SLExpression> list,
Services services) |
SLExpression |
translateSequenceReference(SLExpression receiver,
SLExpression rangeFrom,
SLExpression rangeTo) |
SLExpression |
translateToJDLTerm(java.lang.String functName,
ImmutableList<SLExpression> list) |
SLExpression |
translateToJDLTerm(org.antlr.runtime.Token escape,
java.lang.String functName,
Services services,
TermBuilder tb,
ImmutableList<SLExpression> list) |
protected Term |
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 |
unsignedShiftRight(SLExpression left,
SLExpression right) |
Term |
upperBound(Term a,
LogicVariable lv)
Extracts upper bound from a if it matches the pattern.
|
SLExpression |
values(KeYJavaType t) |