de.uka.ilkd.key.symbolic_execution.profile

Class SymbolicExecutionJavaProfile

java.lang.Object

de.uka.ilkd.key.proof.init.AbstractProfile

de.uka.ilkd.key.proof.init.JavaProfile

de.uka.ilkd.key.symbolic_execution.profile.SymbolicExecutionJavaProfile

All Implemented Interfaces:

Profile

public class SymbolicExecutionJavaProfile
extends JavaProfile

An extended JavaProfile used by the symbolic execution API.

Author:

Martin Hentschel

Field Summary

Fields

Modifier and Type	Field and Description
static SymbolicExecutionJavaProfile	defaultInstance The default instance of this class.
static SymbolicExecutionJavaProfile	defaultInstanceWithTruthValueEvaluation The default instance of this class.
static java.lang.String	NAME The Name of this Profile.
private static StrategyFactory	SYMBOLIC_EXECUTION_FACTORY The used StrategyFactory of the SymbolicExecutionStrategy.
private java.lang.Boolean	truthValueEvaluationEnabled true truth value evaluation is enabled, false truth value evaluation is disabled.

Fields inherited from class de.uka.ilkd.key.proof.init.JavaProfile

DEFAULT, defaultInstancePermissions, NAME_WITH_PERMISSIONS

Constructor Summary

Constructors

Constructor and Description
SymbolicExecutionJavaProfile(boolean predicateEvaluationEnabled) Constructor.

Method Summary

Modifier and Type	Method and Description
protected ImmutableSet<GoalChooserBuilder>	computeSupportedGoalChooserBuilder()
protected ImmutableList<TermLabelManager.TermLabelConfiguration>	computeTermLabelConfiguration() Computes the TermLabelManager.TermLabelConfiguration to use in this Profile.
static SymbolicExecutionJavaProfile	getDefaultInstance() Returns the default instance of this class.
static SymbolicExecutionJavaProfile	getDefaultInstance(boolean truthValueEvaluationEnabled) Returns the default instance of this class.
protected ImmutableSet<StrategyFactory>	getStrategyFactories()
static ImmutableList<TermLabelManager.TermLabelConfiguration>	getSymbolicExecutionTermLabelConfigurations(boolean predicateEvaluationEnabled) Returns the additional TermLabelFactory instances used for symbolic execution.
protected ImmutableList<BuiltInRule>	initBuiltInRules()
protected void	initTermLabelManager() Initializes the TermLabelManager.
boolean	isPredicateEvaluationEnabled() Checks if predicate evaluation is enabled or not.
static boolean	isTruthValueEvaluationEnabled(InitConfig initConfig) Checks if truth value evaluation is enabled in the given InitConfig.
static boolean	isTruthValueEvaluationEnabled(Profile profile) Checks if predicate evaluation is enabled in the given Profile.
static boolean	isTruthValueTracingEnabled(Proof proof) Checks if truth value evaluation is enabled in the given Proof.
java.lang.String	name() the name of the profile

Methods inherited from class de.uka.ilkd.key.proof.init.JavaProfile

getDefaultStrategyFactory, getJustification, getOneStepSimpilifier, isSpecificationInvolvedInRuleApp, withPermissions

Methods inherited from class de.uka.ilkd.key.proof.init.AbstractProfile

getDefaultGoalChooserBuilder, getDefaultProfile, getInternalClassDirectory, getInternalClasslistFilename, getSelectedGoalChooserBuilder, getStandardRules, getStrategyFactory, getTermLabelManager, lookupGC, setDefaultProfile, setSelectedGoalChooserBuilder, supportedGoalChoosers, supportedStrategies, supportsStrategyFactory

Methods inherited from class java.lang.Object

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

Field Detail

NAME

public static final java.lang.String NAME

The Name of this Profile.

See Also:

Constant Field Values

SYMBOLIC_EXECUTION_FACTORY

private static final StrategyFactory SYMBOLIC_EXECUTION_FACTORY

The used StrategyFactory of the SymbolicExecutionStrategy.

truthValueEvaluationEnabled

private final java.lang.Boolean truthValueEvaluationEnabled

true truth value evaluation is enabled, false truth value evaluation is disabled.

defaultInstance

public static SymbolicExecutionJavaProfile defaultInstance

The default instance of this class.

It is typically used in the Thread of the user interface. Other instances of this class are typically only required to use them in different Threads (not the UI Thread).

defaultInstanceWithTruthValueEvaluation

public static SymbolicExecutionJavaProfile defaultInstanceWithTruthValueEvaluation

The default instance of this class.

It is typically used in the Thread of the user interface. Other instances of this class are typically only required to use them in different Threads (not the UI Thread).

Constructor Detail

SymbolicExecutionJavaProfile

public SymbolicExecutionJavaProfile(boolean predicateEvaluationEnabled)

Constructor.

Parameters:

predicateEvaluationEnabled - true predicate evaluation is enabled, false predicate evaluation is disabled.

Method Detail

computeSupportedGoalChooserBuilder

protected ImmutableSet<GoalChooserBuilder> computeSupportedGoalChooserBuilder()

Overrides:

computeSupportedGoalChooserBuilder in class AbstractProfile

initTermLabelManager

protected void initTermLabelManager()

Initializes the TermLabelManager.

Overrides:

initTermLabelManager in class AbstractProfile

computeTermLabelConfiguration

protected ImmutableList<TermLabelManager.TermLabelConfiguration> computeTermLabelConfiguration()

Computes the TermLabelManager.TermLabelConfiguration to use in this Profile.

Overrides:

computeTermLabelConfiguration in class JavaProfile

Returns:

The TermLabelManager.TermLabelConfiguration to use in this Profile.

getSymbolicExecutionTermLabelConfigurations

public static ImmutableList<TermLabelManager.TermLabelConfiguration> getSymbolicExecutionTermLabelConfigurations(boolean predicateEvaluationEnabled)

Returns the additional TermLabelFactory instances used for symbolic execution.

Parameters:

predicateEvaluationEnabled - true predicate evaluation is enabled, false predicate evaluation is disabled.

Returns:

The additional TermLabelFactory instances used for symbolic execution.

getStrategyFactories

protected ImmutableSet<StrategyFactory> getStrategyFactories()

Overrides:

getStrategyFactories in class JavaProfile

initBuiltInRules

protected ImmutableList<BuiltInRule> initBuiltInRules()

Overrides:

initBuiltInRules in class JavaProfile

name

public java.lang.String name()

the name of the profile

Specified by:

name in interface Profile

Overrides:

name in class JavaProfile

Returns:

the name

isPredicateEvaluationEnabled

public boolean isPredicateEvaluationEnabled()

Checks if predicate evaluation is enabled or not.

Returns:

true predicate evaluation is enabled, false predicate evaluation is disabled.

getDefaultInstance

public static SymbolicExecutionJavaProfile getDefaultInstance()

Returns the default instance of this class.

It is typically used in the Thread of the user interface. Other instances of this class are typically only required to use them in different Threads (not the UI Thread).

Returns:

The default instance for usage in the Thread of the user interface.

getDefaultInstance

public static SymbolicExecutionJavaProfile getDefaultInstance(boolean truthValueEvaluationEnabled)

Returns the default instance of this class.

It is typically used in the Thread of the user interface. Other instances of this class are typically only required to use them in different Threads (not the UI Thread).

Parameters:

truthValueEvaluationEnabled - true truth value evaluation is enabled, false truth value evaluation is disabled.

Returns:

The default instance for usage in the Thread of the user interface.

isTruthValueTracingEnabled

public static boolean isTruthValueTracingEnabled(Proof proof)

Checks if truth value evaluation is enabled in the given Proof.

Parameters:

proof - The Proof to check.

Returns:

true truth value evaluation is enabled, false truth value evaluation is disabled.

isTruthValueEvaluationEnabled

public static boolean isTruthValueEvaluationEnabled(InitConfig initConfig)

Checks if truth value evaluation is enabled in the given InitConfig.

Parameters:

initConfig - The InitConfig to check.

Returns:

true truth value evaluation is enabled, false truth value evaluation is disabled.

isTruthValueEvaluationEnabled

public static boolean isTruthValueEvaluationEnabled(Profile profile)

Checks if predicate evaluation is enabled in the given Profile.

Parameters:

profile - The Profile to check.

Returns:

true predicate evaluation is enabled, false predicate evaluation is disabled.