de.uka.ilkd.key.macros

Class FinishSymbolicExecutionUntilMergePointMacro.FilterSymbexStrategy

java.lang.Object

de.uka.ilkd.key.macros.FilterStrategy

de.uka.ilkd.key.macros.FinishSymbolicExecutionUntilMergePointMacro.FilterSymbexStrategy

All Implemented Interfaces:

Named, Feature, Strategy

Enclosing class:

FinishSymbolicExecutionUntilMergePointMacro

private class FinishSymbolicExecutionUntilMergePointMacro.FilterSymbexStrategy
extends FilterStrategy

The Class FilterSymbexStrategy is a special strategy assigning to any rule infinite costs if the goal has no modality or if a merge point is reached.

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private class	FinishSymbolicExecutionUntilMergePointMacro.FilterSymbexStrategy.FindBreakVisitor Visitor for finding out whether there is a break statement contained in a program element.

Field Summary

Fields

Modifier and Type	Field and Description
private Name	NAME

Constructor Summary

Constructors

Constructor and Description
FilterSymbexStrategy(Strategy delegate)

Method Summary

Modifier and Type	Method and Description
private java.util.HashSet<ProgramElement>	findMergePoints(StatementBlock toSearch, Services services) Returns a set of merge points for the given statement block.
private java.util.LinkedList<StatementBlock>	getBodies(Case elem) Returns the bodies for a Case element.
private java.util.LinkedList<StatementBlock>	getBodies(Catch elem) Returns the body for a Catch element.
private java.util.LinkedList<StatementBlock>	getBodies(CatchAllStatement elem) Returns the body for a CatchAllStatement element.
private java.util.LinkedList<StatementBlock>	getBodies(Else elem) Returns the body for an Else element.
private java.util.LinkedList<StatementBlock>	getBodies(Finally elem) Returns the body for a Finally element.
private java.util.LinkedList<StatementBlock>	getBodies(If elem) Returns the bodies for an If element.
private java.util.LinkedList<StatementBlock>	getBodies(LabeledStatement elem) Returns the body for a LabeledStatement element.
private java.util.LinkedList<StatementBlock>	getBodies(LoopStatement elem) Returns the body for a LoopStatement element.
private java.util.LinkedList<StatementBlock>	getBodies(MethodFrame elem) Returns the body for a MethodFrame element.
private java.util.LinkedList<StatementBlock>	getBodies(SourceElement elem) Returns the bodies for various compound statements like if, try, case, etc.
private java.util.LinkedList<StatementBlock>	getBodies(SynchronizedBlock elem) Returns the body for a SynchronizedBlock element.
private java.util.LinkedList<StatementBlock>	getBodies(Then elem) Returns the body for a Then element.
private java.util.LinkedList<StatementBlock>	getBodies(Try elem) Returns the bodies for a Try element.
boolean	isApprovedApp(RuleApp app, PosInOccurrence pio, Goal goal) Re-Evaluate a RuleApp.
boolean	isStopAtFirstNonCloseableGoal() Checks if the Strategy should stop at the first non closeable Goal.
Name	name() returns the name of this element

Methods inherited from class de.uka.ilkd.key.macros.FilterStrategy

computeCost, instantiateApp

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Methods inherited from interface de.uka.ilkd.key.strategy.Strategy

updateStrategySettings

Field Detail

NAME

private final Name NAME

Constructor Detail

FilterSymbexStrategy

public FilterSymbexStrategy(Strategy delegate)

Method Detail

name

public Name name()

Description copied from interface: Named

returns the name of this element

Returns:

the name of the element

isApprovedApp

public boolean isApprovedApp(RuleApp app,
                             PosInOccurrence pio,
                             Goal goal)

Description copied from interface: Strategy

Re-Evaluate a RuleApp. This method is called immediately before a rule is really applied

Specified by:

isApprovedApp in interface Strategy

Overrides:

isApprovedApp in class FilterStrategy

Returns:

true iff the rule should be applied, false otherwise

findMergePoints

private java.util.HashSet<ProgramElement> findMergePoints(StatementBlock toSearch,
                                                          Services services)

Returns a set of merge points for the given statement block. A merge point is the statement in a program directly after an if-then-else or a try-catch-finally block.

Parameters:

toSearch - The statement block to search for merge points.

Returns:

A set of merge points for the given statement block.

getBodies

private java.util.LinkedList<StatementBlock> getBodies(SourceElement elem)

Returns the bodies for various compound statements like if, try, case, etc. If there is no body, an empty list is returned.

Parameters:

elem - The element to return the bodies for.

Returns:

The bodies for the given source element.

getBodies

private java.util.LinkedList<StatementBlock> getBodies(If elem)

Returns the bodies for an If element. NOTE: This includes the bodies for the Then *and* the Else part!

Parameters:

elem - The element to return the bodies for.

Returns:

The bodies for the given source element.

getBodies

private java.util.LinkedList<StatementBlock> getBodies(Then elem)

Returns the body for a Then element.

Parameters:

elem - The element to return the bodies for.

Returns:

The bodies for the given source element.

getBodies

private java.util.LinkedList<StatementBlock> getBodies(Else elem)

Returns the body for an Else element.

Parameters:

elem - The element to return the bodies for.

Returns:

The bodies for the given source element.

getBodies

private java.util.LinkedList<StatementBlock> getBodies(Try elem)

Returns the bodies for a Try element. NOTE: This includes the bodies for Try *and* for the branches!

Parameters:

elem - The element to return the bodies for.

Returns:

The bodies for the given source element.

getBodies

private java.util.LinkedList<StatementBlock> getBodies(Catch elem)

Returns the body for a Catch element.

Parameters:

elem - The element to return the bodies for.

Returns:

The bodies for the given source element.

getBodies

private java.util.LinkedList<StatementBlock> getBodies(Finally elem)

Returns the body for a Finally element.

Parameters:

elem - The element to return the bodies for.

Returns:

The bodies for the given source element.

getBodies

private java.util.LinkedList<StatementBlock> getBodies(MethodFrame elem)

Returns the body for a MethodFrame element.

Parameters:

elem - The element to return the bodies for.

Returns:

The bodies for the given source element.

getBodies

private java.util.LinkedList<StatementBlock> getBodies(Case elem)

Returns the bodies for a Case element.

Parameters:

elem - The element to return the bodies for.

Returns:

The bodies for the given source element.

getBodies

private java.util.LinkedList<StatementBlock> getBodies(CatchAllStatement elem)

Returns the body for a CatchAllStatement element.

Parameters:

elem - The element to return the bodies for.

Returns:

The bodies for the given source element.

getBodies

private java.util.LinkedList<StatementBlock> getBodies(LabeledStatement elem)

Returns the body for a LabeledStatement element.

Parameters:

elem - The element to return the bodies for.

Returns:

The bodies for the given source element.

getBodies

private java.util.LinkedList<StatementBlock> getBodies(LoopStatement elem)

Returns the body for a LoopStatement element.

Parameters:

elem - The element to return the bodies for.

Returns:

The bodies for the given source element.

getBodies

private java.util.LinkedList<StatementBlock> getBodies(SynchronizedBlock elem)

Returns the body for a SynchronizedBlock element.

Parameters:

elem - The element to return the bodies for.

Returns:

The bodies for the given source element.

isStopAtFirstNonCloseableGoal

public boolean isStopAtFirstNonCloseableGoal()

Description copied from interface: Strategy

Checks if the Strategy should stop at the first non closeable Goal.

Returns:

true stop, false continue on other Goals.