public abstract class JoinProcedure extends Object
For example, computing the join result for a variable x in one state where x is 42 and another one where x is 17, the result could be the update x := c, where c is constrained to be positive by a formula in the returned constraints set.
New join procedures need to be registered in the list CONCRETE_RULES!
JoinIfThenElse
,
JoinIfThenElseAntecedent
,
JoinWeaken
,
JoinWithSignLattice
Modifier and Type | Field and Description |
---|---|
(package private) static ImmutableList<JoinProcedure> |
CONCRETE_RULES
Concrete join procedures.
|
Constructor and Description |
---|
JoinProcedure() |
Modifier and Type | Method and Description |
---|---|
static ImmutableList<JoinProcedure> |
getJoinProcedures()
Returns all registered join procedures.
|
static JoinProcedure |
getProcedureByName(String procName)
Returns the join procedure for the given name.
|
abstract 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.
|
abstract boolean |
requiresDistinguishablePathConditions() |
static ImmutableList<JoinProcedure> CONCRETE_RULES
public abstract Triple<ImmutableSet<Term>,Term,ImmutableSet<Name>> joinValuesInStates(Term v, SymbolicExecutionState state1, Term valueInState1, SymbolicExecutionState state2, Term valueInState2, Term distinguishingFormula, Services services)
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 abstract boolean requiresDistinguishablePathConditions()
public static JoinProcedure getProcedureByName(String procName)
procName
- Name of the join procedure.public static ImmutableList<JoinProcedure> getJoinProcedures()