public static class SymbolicExecutionStrategy.Factory extends java.lang.Object implements StrategyFactory
StrategyFactory
to create instances of SymbolicExecutionStrategy
.Modifier and Type | Field and Description |
---|---|
static java.lang.String |
ALIAS_CHECK_IMMEDIATELY
Shown string for alias check "Immediately".
|
static java.lang.String |
ALIAS_CHECK_NEVER
Shown string for alias check "Never".
|
static java.lang.String |
BLOCK_TREATMENT_EXPAND
Shown string for block treatment "Expand".
|
static java.lang.String |
BLOCK_TREATMENT_INVARIANT
Shown string for block treatment "Invariant".
|
static java.lang.String |
LOOP_TREATMENT_EXPAND
Shown string for loop treatment "Expand".
|
static java.lang.String |
LOOP_TREATMENT_INVARIANT
Shown string for loop treatment "Invariant".
|
static java.lang.String |
METHOD_TREATMENT_CONTRACT
Shown string for method treatment "Contract".
|
static java.lang.String |
METHOD_TREATMENT_EXPAND
Shown string for method treatment "Expand".
|
static java.lang.String |
NON_EXECUTION_BRANCH_HIDING_OFF
Shown string for alias check "Never".
|
static java.lang.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 java.lang.String METHOD_TREATMENT_EXPAND
public static final java.lang.String METHOD_TREATMENT_CONTRACT
public static final java.lang.String LOOP_TREATMENT_EXPAND
public static final java.lang.String LOOP_TREATMENT_INVARIANT
public static final java.lang.String BLOCK_TREATMENT_EXPAND
public static final java.lang.String BLOCK_TREATMENT_INVARIANT
public static final java.lang.String NON_EXECUTION_BRANCH_HIDING_OFF
public static final java.lang.String NON_EXECUTION_BRANCH_HIDING_SIDE_PROOF
public static final java.lang.String ALIAS_CHECK_NEVER
public static final java.lang.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.