public abstract class JoinWithLatticeAbstraction extends JoinProcedure
Modifier and Type | Field and Description |
---|---|
private static int |
AXIOM_PROVE_TIMEOUT_MS
Time in milliseconds after which a proof attempt of
a defining axiom times out.
|
Constructor and Description |
---|
JoinWithLatticeAbstraction() |
Modifier and Type | Method and Description |
---|---|
private AbstractDomainElement |
determineAbstractElem(SymbolicExecutionState state,
Term term,
AbstractDomainLattice<?> lattice,
Services services)
Determines the abstract element suitable for the given term.
|
protected abstract AbstractDomainLattice<?> |
getAbstractDomainForSort(Sort s,
Services services)
Returns the abstract domain lattice for the given sort or null if there
has no lattice been specified for that sort.
|
Triple<ImmutableSet<Term>,Term,ImmutableSet<Name>> |
joinValuesInStates(Term v,
SymbolicExecutionState state1,
Term valueInState1,
SymbolicExecutionState state2,
Term valueInState2,
Term distinguishingFormula,
Services services)
Joins two values valueInState1 and valueInState2 of corresponding SE
states state1 and state2 to a new value of a join state.
|
boolean |
requiresDistinguishablePathConditions() |
getJoinProcedures, getProcedureByName
private static final int AXIOM_PROVE_TIMEOUT_MS
protected abstract AbstractDomainLattice<?> getAbstractDomainForSort(Sort s, Services services)
s
- The sort to return the matching lattice for.services
- The services object.public Triple<ImmutableSet<Term>,Term,ImmutableSet<Name>> joinValuesInStates(Term v, SymbolicExecutionState state1, Term valueInState1, SymbolicExecutionState state2, Term valueInState2, Term distinguishingFormula, Services services)
JoinProcedure
joinValuesInStates
in class JoinProcedure
v
- The variable for which the values should be joinedstate1
- First SE state.valueInState1
- Value in state1.state2
- Second SE state.valueInState2
- Value in state2.distinguishingFormula
- The user-specified distinguishing formula. May be null (for
automatic generation).services
- The services object.public boolean requiresDistinguishablePathConditions()
requiresDistinguishablePathConditions
in class JoinProcedure
private AbstractDomainElement determineAbstractElem(SymbolicExecutionState state, Term term, AbstractDomainLattice<?> lattice, Services services)
state
- State in which the evaluation of the defining axioms should be
tested.term
- The term to find an abstract description for.lattice
- The underlying abstract domain.services
- The services object.