private class FinishSymbolicExecutionWithSpecJoinsMacro.FilterSymbexStrategy extends FilterStrategy
Modifier and Type | Field and Description |
---|---|
private HashSet<JavaBlock> |
alreadySeen |
private HashSet<ProgramElement> |
breakpoints |
private HashMap<ProgramElement,Node> |
commonParents |
private boolean |
enforceJoin |
private HashMap<ProgramElement,BlockContract> |
joinContracts |
private Pair<Goal,JoinRuleBuiltInRuleApp> |
joinInformation |
private Name |
NAME |
private HashSet<Goal> |
stoppedGoals |
Constructor and Description |
---|
FilterSymbexStrategy(Strategy delegate)
Creates a new FilterSymbexStrategy based on the given delegate.
|
Modifier and Type | Method and Description |
---|---|
private HashSet<ProgramElement> |
findJoinPoints(StatementBlock toSearch,
Goal goal)
Returns a set of join points for the given statement block.
|
Pair<Goal,JoinRuleBuiltInRuleApp> |
getAndResetJoinInformation()
Returns the information for a join to apply if applicable, or null if
there is no join to execute.
|
private Pair<BlockContract,Statement> |
getBlockContractFor(Statement stmt,
Services services)
Obtains the pair of block contract containing a join specification
and the corresponding breakpoint, if any, for the given statement.
|
private Statement |
getBreakPoint(Semisequent succedent,
Services services) |
private PosInOccurrence |
getPioForBreakpoint(Statement breakpoint,
Sequent sequent)
Returns the
PosInOccurrence for the given breakpoint
statement inside the given sequent, or null if the statement does not
exist within the sequent. |
private boolean |
hasBreakPoint(Semisequent succedent,
Services services,
Statement breakpoint) |
private boolean |
hasStmtForWhichPredicateHolds(Semisequent succedent,
Services services,
FinishSymbolicExecutionWithSpecJoinsMacro.Predicate<Statement> pred) |
boolean |
isApprovedApp(RuleApp app,
PosInOccurrence pio,
Goal goal)
Re-Evaluate a
RuleApp . |
boolean |
isStopAtFirstNonCloseableGoal()
|
Name |
name()
returns the name of this element
|
computeCost, instantiateApp
private final Name NAME
private boolean enforceJoin
private Pair<Goal,JoinRuleBuiltInRuleApp> joinInformation
private HashSet<ProgramElement> breakpoints
private HashMap<ProgramElement,Node> commonParents
private HashMap<ProgramElement,BlockContract> joinContracts
public FilterSymbexStrategy(Strategy delegate)
delegate
- The strategy to wrap.public Pair<Goal,JoinRuleBuiltInRuleApp> getAndResetJoinInformation()
public Name name()
Named
public boolean isApprovedApp(RuleApp app, PosInOccurrence pio, Goal goal)
Strategy
RuleApp
. This method is
called immediately before a rule is really appliedisApprovedApp
in interface Strategy
isApprovedApp
in class FilterStrategy
public boolean isStopAtFirstNonCloseableGoal()
Strategy
true
stop, false
continue on other Goal
s.private PosInOccurrence getPioForBreakpoint(Statement breakpoint, Sequent sequent)
PosInOccurrence
for the given breakpoint
statement inside the given sequent, or null if the statement does not
exist within the sequent. The returned PosInOccurrence
is the
top level formula inside the sequent containing the breakpoint
statement.breakpoint
- The statement to locate inside the sequent.sequent
- The sequent to find the statement in.private HashSet<ProgramElement> findJoinPoints(StatementBlock toSearch, Goal goal)
toSearch
- The statement block to search for join points.goal
- The goal corresponding to the statement block.private Pair<BlockContract,Statement> getBlockContractFor(Statement stmt, Services services)
stmt
- Statement to find a contract and breakpoint for. This
should be the whole "program counter", i.e. the next
statement that will be the breakpoint should also be
included.services
- The services object.private Statement getBreakPoint(Semisequent succedent, Services services)
succedent
- Succedent of a sequent.private boolean hasBreakPoint(Semisequent succedent, Services services, Statement breakpoint)
succedent
- Succedent of a sequent.private boolean hasStmtForWhichPredicateHolds(Semisequent succedent, Services services, FinishSymbolicExecutionWithSpecJoinsMacro.Predicate<Statement> pred)
succedent
- Succedent of a sequent.pred
- A decision predicate.