All Methods Static Methods Instance Methods Concrete Methods
Modifier and Type |
Method and Description |
void |
add(Named symb) |
void |
add(Term t) |
private void |
addFunc(Function f,
boolean labeled) |
private void |
addFunction(Function f,
boolean labeled) |
void |
addLabeled(Named symb) |
void |
addLabeled(Term t) |
void |
addLabeledTotalTerm(Term t) |
private void |
addPredicate(Function p,
boolean labeled) |
private void |
addProgramVariable(ProgramVariable pv,
boolean labeled) |
private void |
addSchemaVariable(SchemaVariable sv,
boolean labeled) |
private void |
addSort(Sort s,
boolean labeled) |
private void |
addTaclet(Taclet t,
boolean labeled) |
void |
addTotalTerm(Term t) |
private boolean |
containsFunction(Function f) |
private boolean |
containsPredicate(Function f) |
private boolean |
containsProgramVariable(ProgramVariable pv) |
private boolean |
containsSchemaVariable(SchemaVariable sv) |
private boolean |
containsSort(Sort s) |
private boolean |
containsTaclet(Taclet t) |
private java.util.LinkedList<Sort> |
ensureRightOrderOfSorts(ImmutableSet<Sort> s) |
private ImmutableSet<Function> |
getFunctions() |
private ImmutableSet<Pair<Function,java.lang.Boolean>> |
getLabeledFunctions() |
private ImmutableSet<Pair<Function,java.lang.Boolean>> |
getLabeledPredicates() |
private ImmutableSet<Pair<ProgramVariable,java.lang.Boolean>> |
getLabeledProgramVariables() |
private ImmutableSet<Pair<SchemaVariable,java.lang.Boolean>> |
getLabeledSchemaVariables() |
private ImmutableSet<Pair<Sort,java.lang.Boolean>> |
getLabeledSorts() |
private InfFlowProofSymbols |
getLabeledSymbols() |
private ImmutableSet<Pair<Taclet,java.lang.Boolean>> |
getLabeledTaclets() |
private ImmutableSet<Function> |
getPredicates() |
private ImmutableSet<ProgramVariable> |
getProgramVariables() |
private ImmutableSet<SchemaVariable> |
getSchemaVariables() |
private ImmutableSet<Sort> |
getSorts() |
private ImmutableSet<Taclet> |
getTaclets() |
boolean |
isFreshContract() |
private boolean |
isPredicate(Operator f) |
private java.lang.String |
printFunctions() |
private java.lang.String |
printPredicates() |
private java.lang.String |
printProgramVariables() |
java.lang.String |
printProofSymbols() |
private java.lang.String |
printSchemaVariables() |
private java.lang.String |
printSorts() |
private java.lang.String |
printSpace() |
private java.lang.String |
printTaclets() |
private java.util.LinkedList<Sort> |
removeArraySorts(java.util.LinkedList<Sort> sorts) |
static ProgramVariable |
searchPV(java.lang.String s,
Services services) |
InfFlowProofSymbols |
union(InfFlowProofSymbols symbols) |
InfFlowProofSymbols |
unionLabeled(InfFlowProofSymbols symbols) |
void |
useProofSymbols() |