public class SymbolicExecutionEnvironment<U extends UserInterfaceControl> extends KeYEnvironment<U>
Proof
s
via an SymbolicExecutionTreeBuilder
.Modifier and Type | Field and Description |
---|---|
private SymbolicExecutionTreeBuilder |
builder
The
SymbolicExecutionTreeBuilder for execution tree extraction. |
Constructor and Description |
---|
SymbolicExecutionEnvironment(KeYEnvironment<U> environment,
SymbolicExecutionTreeBuilder builder)
Constructor.
|
SymbolicExecutionEnvironment(U ui,
InitConfig initConfig,
SymbolicExecutionTreeBuilder builder)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
static void |
configureProofForSymbolicExecution(Proof proof,
int maximalNumberOfNodesPerBranch)
Configures the given
Proof to use the symbolic execution strategy
by reusing the default StrategyProperties . |
static void |
configureProofForSymbolicExecution(Proof proof,
int maximalNumberOfNodesPerBranch,
boolean methodTreatmentContract,
boolean loopTreatmentInvariant,
boolean blockTreatmentContract,
boolean nonExecutionBranchHidingSideProofs,
boolean aliasChecks)
Configures the given
Proof to use the symbolic execution strategy. |
void |
dispose()
Disposes this
KeYEnvironment . |
SymbolicExecutionTreeBuilder |
getBuilder()
Returns the
SymbolicExecutionTreeBuilder for execution tree extraction. |
Proof |
getProof()
Returns the
Proof of getBuilder() . |
createProof, getInitConfig, getJavaInfo, getLoadedProof, getProfile, getProofControl, getProofScript, getReplayResult, getServices, getSpecificationRepository, getUi, isDisposed, load, load, load, load, load
private SymbolicExecutionTreeBuilder builder
SymbolicExecutionTreeBuilder
for execution tree extraction.public SymbolicExecutionEnvironment(KeYEnvironment<U> environment, SymbolicExecutionTreeBuilder builder)
environment
- The parent KeYEnvironment
.builder
- The SymbolicExecutionTreeBuilder
for execution tree extraction.public SymbolicExecutionEnvironment(U ui, InitConfig initConfig, SymbolicExecutionTreeBuilder builder)
ui
- The UserInterfaceControl
in which the Proof
is loaded.initConfig
- The loaded project.builder
- The SymbolicExecutionTreeBuilder
for execution tree extraction.public SymbolicExecutionTreeBuilder getBuilder()
SymbolicExecutionTreeBuilder
for execution tree extraction.SymbolicExecutionTreeBuilder
for execution tree extraction.public Proof getProof()
Proof
of getBuilder()
.Proof
of getBuilder()
.public static void configureProofForSymbolicExecution(Proof proof, int maximalNumberOfNodesPerBranch)
Proof
to use the symbolic execution strategy
by reusing the default StrategyProperties
.proof
- The Proof
to configure.maximalNumberOfNodesPerBranch
- The maximal number of nodes per branch.public static void configureProofForSymbolicExecution(Proof proof, int maximalNumberOfNodesPerBranch, boolean methodTreatmentContract, boolean loopTreatmentInvariant, boolean blockTreatmentContract, boolean nonExecutionBranchHidingSideProofs, boolean aliasChecks)
Proof
to use the symbolic execution strategy.proof
- The Proof
to configure.maximalNumberOfNodesPerBranch
- The maximal number of nodes per branch.methodTreatmentContract
- true
use operation contracts, false
expand methods.loopTreatmentInvariant
- true
use invariants, false
expand loops.blockTreatmentContract
- Block contracts or expand otherwise?nonExecutionBranchHidingSideProofs
- true
hide non execution branch labels by side proofs, false
do not hide execution branch labels.aliasChecks
- Do alias checks?public void dispose()
KeYEnvironment
.dispose
in class KeYEnvironment<U extends UserInterfaceControl>