public abstract class MergeProcedure
extends java.lang.Object
For example, computing the merge 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 merge procedures need to be registered in the list CONCRETE_RULES!
MergeByIfThenElse
,
MergeIfThenElseAntecedent
,
MergeTotalWeakening
,
MergeWithSignLattice
Modifier and Type | Class and Description |
---|---|
static class |
MergeProcedure.ValuesMergeResult
Encapsulates the result of a merge of values.
|
Modifier and Type | Field and Description |
---|---|
(package private) static ImmutableList<MergeProcedure> |
CONCRETE_RULES
Concrete merge procedures.
|
Constructor and Description |
---|
MergeProcedure() |
Modifier and Type | Method and Description |
---|---|
abstract boolean |
complete()
Similar to
AbstractBuiltInRuleApp.complete() . |
static ImmutableList<MergeProcedure> |
getMergeProcedures()
Returns all registered merge procedures.
|
static MergeProcedure |
getProcedureByName(java.lang.String procName)
Returns the merge procedure for the given name.
|
abstract MergeProcedure.ValuesMergeResult |
mergeValuesInStates(Term v,
SymbolicExecutionState state1,
Term valueInState1,
SymbolicExecutionState state2,
Term valueInState2,
Term distinguishingFormula,
Services services)
Merges two values valueInState1 and valueInState2 of corresponding SE
states state1 and state2 to a new value of a merge state.
|
abstract boolean |
requiresDistinguishablePathConditions() |
static ImmutableList<MergeProcedure> CONCRETE_RULES
public abstract MergeProcedure.ValuesMergeResult mergeValuesInStates(Term v, SymbolicExecutionState state1, Term valueInState1, SymbolicExecutionState state2, Term valueInState2, Term distinguishingFormula, Services services)
v
- The variable for which the values should be mergedstate1
- 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 complete()
AbstractBuiltInRuleApp.complete()
. Method was
introduced for predicate abstraction (which is not complete if the
abstraction predicates are not set).public abstract boolean requiresDistinguishablePathConditions()
public static MergeProcedure getProcedureByName(java.lang.String procName)
procName
- Name of the merge procedure.public static ImmutableList<MergeProcedure> getMergeProcedures()