public static class SymbolicExecutionStrategy.Factory extends Object implements StrategyFactory
StrategyFactory
to create instances of SymbolicExecutionStrategy
.Modifier and Type | Field and Description |
---|---|
static String |
ALIAS_CHECK_IMMEDIATELY
Shown string for alias check "Immediately".
|
static String |
ALIAS_CHECK_NEVER
Shown string for alias check "Never".
|
static String |
BLOCK_TREATMENT_EXPAND
Shown string for block treatment "Expand".
|
static String |
BLOCK_TREATMENT_INVARIANT
Shown string for block treatment "Invariant".
|
static String |
LOOP_TREATMENT_EXPAND
Shown string for loop treatment "Expand".
|
static String |
LOOP_TREATMENT_INVARIANT
Shown string for loop treatment "Invariant".
|
static String |
METHOD_TREATMENT_CONTRACT
Shown string for method treatment "Contract".
|
static String |
METHOD_TREATMENT_EXPAND
Shown string for method treatment "Expand".
|
static String |
NON_EXECUTION_BRANCH_HIDING_OFF
Shown string for alias check "Never".
|
static String |
NON_EXECUTION_BRANCH_HIDING_SIDE_PROOF
Shown string for alias check "Immediately".
|
Constructor and Description |
---|
Factory() |
Modifier and Type | Method and Description |
---|---|
Strategy |
create(Proof proof,
StrategyProperties sp)
Create strategy for a proof.
|
StrategySettingsDefinition |
getSettingsDefinition()
Returns the
StrategySettingsDefinition which describes
how an user interface has to look like to edit StrategySettings
supported by created Strategy instances. |
Name |
name()
returns the name of this element
|
public static final String METHOD_TREATMENT_EXPAND
public static final String METHOD_TREATMENT_CONTRACT
public static final String LOOP_TREATMENT_EXPAND
public static final String LOOP_TREATMENT_INVARIANT
public static final String BLOCK_TREATMENT_EXPAND
public static final String BLOCK_TREATMENT_INVARIANT
public static final String NON_EXECUTION_BRANCH_HIDING_OFF
public static final String NON_EXECUTION_BRANCH_HIDING_SIDE_PROOF
public static final String ALIAS_CHECK_NEVER
public static final String ALIAS_CHECK_IMMEDIATELY
public Strategy create(Proof proof, StrategyProperties sp)
create
in interface StrategyFactory
proof
- the Proof a strategy is created forsp
- the StrategyProperties to customize the
strategypublic Name name()
public StrategySettingsDefinition getSettingsDefinition()
StrategySettingsDefinition
which describes
how an user interface has to look like to edit StrategySettings
supported by created Strategy
instances.getSettingsDefinition
in interface StrategyFactory
StrategySettingsDefinition
which describes the user interface.