de.uka.ilkd.key.symbolic_execution.util

Class SymbolicExecutionEnvironment<U extends UserInterfaceControl>

java.lang.Object

de.uka.ilkd.key.control.KeYEnvironment<U>

de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionEnvironment<U>

public class SymbolicExecutionEnvironment<U extends UserInterfaceControl>
extends KeYEnvironment<U>

Instances of this class are used to collect and access all relevant information for symbolic execution tree extraction of Proofs via an SymbolicExecutionTreeBuilder.

Author:

Martin Hentschel

Field Summary

Fields

Modifier and Type	Field and Description
private SymbolicExecutionTreeBuilder	builder The SymbolicExecutionTreeBuilder for execution tree extraction.

Constructor Summary

Constructors

Constructor and Description
SymbolicExecutionEnvironment(KeYEnvironment<U> environment, SymbolicExecutionTreeBuilder builder) Constructor.
SymbolicExecutionEnvironment(U ui, InitConfig initConfig, SymbolicExecutionTreeBuilder builder) Constructor.

Method Summary

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().

Methods inherited from class de.uka.ilkd.key.control.KeYEnvironment

createProof, getInitConfig, getJavaInfo, getLoadedProof, getProfile, getProofControl, getProofScript, getReplayResult, getServices, getSpecificationRepository, getUi, isDisposed, load, load, load, load, load

Methods inherited from class java.lang.Object

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

Field Detail

builder

private SymbolicExecutionTreeBuilder builder

The SymbolicExecutionTreeBuilder for execution tree extraction.

Constructor Detail

SymbolicExecutionEnvironment

public SymbolicExecutionEnvironment(KeYEnvironment<U> environment,
                                    SymbolicExecutionTreeBuilder builder)

Constructor.

Parameters:

environment - The parent KeYEnvironment.

builder - The SymbolicExecutionTreeBuilder for execution tree extraction.

SymbolicExecutionEnvironment

public SymbolicExecutionEnvironment(U ui,
                                    InitConfig initConfig,
                                    SymbolicExecutionTreeBuilder builder)

Constructor.

Parameters:

ui - The UserInterfaceControl in which the Proof is loaded.

initConfig - The loaded project.

builder - The SymbolicExecutionTreeBuilder for execution tree extraction.

Method Detail

getBuilder

public SymbolicExecutionTreeBuilder getBuilder()

Returns the SymbolicExecutionTreeBuilder for execution tree extraction.

Returns:

The SymbolicExecutionTreeBuilder for execution tree extraction.

getProof

public Proof getProof()

Returns the Proof of getBuilder().

Returns:

The Proof of getBuilder().

configureProofForSymbolicExecution

public static void configureProofForSymbolicExecution(Proof proof,
                                                      int maximalNumberOfNodesPerBranch)

Configures the given Proof to use the symbolic execution strategy by reusing the default StrategyProperties.

Parameters:

proof - The Proof to configure.

maximalNumberOfNodesPerBranch - The maximal number of nodes per branch.

configureProofForSymbolicExecution

public 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.

Parameters:

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?

dispose

public void dispose()

Disposes this KeYEnvironment.

Overrides:

dispose in class KeYEnvironment<U extends UserInterfaceControl>