Methods
Modifier and Type |
Method and Description |
private static OracleTerm |
and(OracleTerm left,
OracleTerm right) |
private OracleMethod |
createDummyInvariant(Sort s) |
private OracleMethod |
createDummyOracleMethod(ProgramMethod pm) |
private String |
createExistsBody(QuantifiableVariable qv,
String setName,
OracleTerm cond) |
private String |
createForallBody(QuantifiableVariable qv,
String setName,
OracleUnaryTerm neg) |
private OracleMethod |
createIfThenElseMethod(Term term,
boolean initialSelect) |
private OracleMethod |
createInvariantMethod(Sort s,
boolean initialSelect) |
private String |
createLocationString(OracleTerm heapTerm,
OracleTerm objTerm,
String fieldName,
Sort objSort,
Sort fieldSort,
boolean initialSelect) |
private OracleMethod |
createQuantifierMethod(Term term,
boolean initialSelect) |
private Sort |
createSetSort(String inner) |
private static OracleTerm |
eq(OracleTerm left,
OracleTerm right) |
private void |
findConstants(Set<Term> constants,
Term term) |
static String |
generateMethodName() |
OracleTerm |
generateOracle(Term term,
boolean initialSelect) |
OracleMethod |
generateOracleMethod(Term term) |
Set<Term> |
getConstants() |
private Set<Term> |
getConstants(Term t) |
List<OracleVariable> |
getMethodArgs() |
private List<OracleVariable> |
getMethodArgs(Term t) |
OracleLocationSet |
getOracleLocationSet(Term modifierset) |
Set<OracleMethod> |
getOracleMethods() |
Set<String> |
getPrestateTerms() |
private String |
getSetName(Sort s) |
private String |
getSortInvName(Sort s) |
private void |
initFalse() |
private void |
initOps() |
private void |
initTrue() |
private boolean |
isFalseConstant(Operator o) |
private boolean |
isPreHeap(OracleTerm heapTerm) |
private boolean |
isRelevantConstant(Term c) |
private boolean |
isTrueConstant(Operator o) |
private static OracleTerm |
neg(OracleTerm t) |
private static OracleTerm |
or(OracleTerm left,
OracleTerm right) |
private OracleTerm |
translateFunction(Term term,
boolean initialSelect) |
private OracleTerm |
translateQuery(Term term,
boolean initialSelect,
Operator op) |
private OracleTerm |
translateSelect(Term term,
boolean initialSelect) |