Package | Description |
---|---|
de.uka.ilkd.key.axiom_abstraction | |
de.uka.ilkd.key.rule.merge | |
de.uka.ilkd.key.rule.merge.procedures | |
de.uka.ilkd.key.util.mergerule |
Modifier and Type | Method and Description |
---|---|
AbstractDomainElement |
AbstractDomainLattice.abstractFrom(SymbolicExecutionState state,
Term term,
Services services)
Abstracts from a given element of the concrete domain by returning a
suitable abstract element.
|
static Term |
AbstractDomainLattice.getSideConditionForAxiom(SymbolicExecutionState state,
Term term,
AbstractDomainElement elem,
Services services)
Returns a side condition which has to hold if elem is a correct
abstraction for term.
|
Modifier and Type | Method and Description |
---|---|
SymbolicExecutionState |
CloseAfterMergeRuleBuiltInRuleApp.getMergeState() |
SymbolicExecutionState |
CloseAfterMergeRuleBuiltInRuleApp.getPartnerSEState() |
Modifier and Type | Method and Description |
---|---|
ImmutableList<SymbolicExecutionState> |
MergeRuleBuiltInRuleApp.getMergePartnerStates() |
protected Triple<SymbolicExecutionState,java.util.LinkedHashSet<Name>,java.util.LinkedHashSet<Term>> |
MergeRule.mergeStates(MergeProcedure mergeRule,
SymbolicExecutionState state1,
SymbolicExecutionState state2,
Term programCounter,
Term distinguishingFormula,
Services services)
Merges two SE states (U1,C1,p) and (U2,C2,p) according to the method
MergeRule#mergeValuesInStates(LocationVariable, SymbolicExecutionState, Term, SymbolicExecutionState, Term, Services)
. |
Modifier and Type | Method and Description |
---|---|
CloseAfterMergeRuleBuiltInRuleApp |
CloseAfterMerge.createApp(PosInOccurrence pio,
Node thePartnerNode,
Node correspondingMergeNode,
SymbolicExecutionState mergeNodeState,
SymbolicExecutionState partnerState,
Term pc,
java.util.Set<Name> newNames)
Creates a complete CloseAfterMergeBuiltInRuleApp.
|
protected MergeProcedure.ValuesMergeResult |
MergeRule.mergeHeaps(MergeProcedure mergeRule,
LocationVariable heapVar,
Term heap1,
Term heap2,
SymbolicExecutionState state1,
SymbolicExecutionState state2,
Term distinguishingFormula,
Services services)
Merges two heaps in a zip-like procedure.
|
protected Triple<SymbolicExecutionState,java.util.LinkedHashSet<Name>,java.util.LinkedHashSet<Term>> |
MergeRule.mergeStates(MergeProcedure mergeRule,
SymbolicExecutionState state1,
SymbolicExecutionState state2,
Term programCounter,
Term distinguishingFormula,
Services services)
Merges two SE states (U1,C1,p) and (U2,C2,p) according to the method
MergeRule#mergeValuesInStates(LocationVariable, SymbolicExecutionState, Term, SymbolicExecutionState, Term, Services)
. |
abstract MergeProcedure.ValuesMergeResult |
MergeProcedure.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.
|
void |
CloseAfterMergeRuleBuiltInRuleApp.setMergeNodeState(SymbolicExecutionState mergeState) |
void |
CloseAfterMergeRuleBuiltInRuleApp.setPartnerState(SymbolicExecutionState thisSEState) |
Constructor and Description |
---|
CloseAfterMergeRuleBuiltInRuleApp(BuiltInRule builtInRule,
PosInOccurrence pio,
Node thePartnerNode,
Node correspondingMergeNode,
SymbolicExecutionState mergeNodeState,
SymbolicExecutionState partnerState,
Term pc,
java.util.Set<Name> newNames) |
Constructor and Description |
---|
MergeRuleBuiltInRuleApp(BuiltInRule rule,
PosInOccurrence pio,
ImmutableList<PosInOccurrence> ifInsts,
Node mergeNode,
ImmutableList<MergePartner> mergePartners,
MergeProcedure concreteRule,
SymbolicExecutionStateWithProgCnt thisSEState,
ImmutableList<SymbolicExecutionState> mergePartnerStates,
Term distForm,
java.util.ArrayList<MergeRule.MergeRuleProgressListener> progressListeners) |
Modifier and Type | Method and Description |
---|---|
static Term |
MergeByIfThenElse.createIfThenElseTerm(SymbolicExecutionState state1,
SymbolicExecutionState state2,
Term ifTerm,
Term elseTerm,
Term distinguishingFormula,
Services services)
Creates an if-then-else term for the variable v.
|
MergeProcedure.ValuesMergeResult |
MergeWithLatticeAbstraction.mergeValuesInStates(Term v,
SymbolicExecutionState state1,
Term valueInState1,
SymbolicExecutionState state2,
Term valueInState2,
Term distinguishingFormula,
Services services) |
MergeProcedure.ValuesMergeResult |
MergeWithPredicateAbstractionFactory.mergeValuesInStates(Term v,
SymbolicExecutionState state1,
Term valueInState1,
SymbolicExecutionState state2,
Term valueInState2,
Term distinguishingFormula,
Services services) |
MergeProcedure.ValuesMergeResult |
MergeIfThenElseAntecedent.mergeValuesInStates(Term v,
SymbolicExecutionState state1,
Term valueInState1,
SymbolicExecutionState state2,
Term valueInState2,
Term distinguishingFormula,
Services services) |
MergeProcedure.ValuesMergeResult |
MergeTotalWeakening.mergeValuesInStates(Term v,
SymbolicExecutionState state1,
Term valueInState1,
SymbolicExecutionState state2,
Term valueInState2,
Term distinguishingFormula,
Services services) |
MergeProcedure.ValuesMergeResult |
MergeByIfThenElse.mergeValuesInStates(Term v,
SymbolicExecutionState state1,
Term valueInState1,
SymbolicExecutionState state2,
Term valueInState2,
Term distinguishingFormula,
Services services) |
Modifier and Type | Method and Description |
---|---|
static SymbolicExecutionState |
MergeRuleUtils.sequentToSEPair(Node node,
PosInOccurrence pio,
Services services)
Converts a sequent (given by goal & pos in occurrence) to an SE state
(U,C).
|
SymbolicExecutionState |
SymbolicExecutionStateWithProgCnt.toSymbolicExecutionState() |
Modifier and Type | Method and Description |
---|---|
static Pair<SymbolicExecutionState,SymbolicExecutionState> |
MergeRuleUtils.handleNameClashes(SymbolicExecutionState mergeState,
SymbolicExecutionState mergePartnerState,
Services services)
Due to the introduction of local namespaces, we run into trouble when
applying state merging in the presence of locally introduced symbols.
|
static Pair<SymbolicExecutionState,SymbolicExecutionState> |
MergeRuleUtils.handleNameClashes(SymbolicExecutionState mergeState,
SymbolicExecutionState mergePartnerState,
Services services)
Due to the introduction of local namespaces, we run into trouble when
applying state merging in the presence of locally introduced symbols.
|
static ImmutableList<SymbolicExecutionState> |
MergeRuleUtils.sequentsToSEPairs(java.lang.Iterable<MergePartner> sequentInfos)
Convenience method for converting a whole list of goal-pio combinations
to symbolic execution states; relies on
MergeRuleUtils.sequentToSETriple(Node, PosInOccurrence, Services) . |
Modifier and Type | Method and Description |
---|---|
static void |
MergeRuleUtils.closeMergePartnerGoal(Node mergeNodeParent,
Goal mergePartner,
PosInOccurrence pio,
SymbolicExecutionState mergeState,
SymbolicExecutionState mergePartnerState,
Term pc,
java.util.Set<Name> newNames)
Closes the given partner goal, using the
CloseAfterMerge rule. |
static Pair<SymbolicExecutionState,SymbolicExecutionState> |
MergeRuleUtils.handleNameClashes(SymbolicExecutionState mergeState,
SymbolicExecutionState mergePartnerState,
Services services)
Due to the introduction of local namespaces, we run into trouble when
applying state merging in the presence of locally introduced symbols.
|
Copyright © 2003-2019 The KeY-Project.