public class SymbolicExecutionJavaProfile extends JavaProfile
JavaProfile
used by the symbolic execution API.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
|
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. |
DEFAULT, defaultInstancePermissions, NAME_WITH_PERMISSIONS
Constructor and Description |
---|
SymbolicExecutionJavaProfile(boolean predicateEvaluationEnabled)
Constructor.
|
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
|
getDefaultStrategyFactory, getJustification, getOneStepSimpilifier, isSpecificationInvolvedInRuleApp, withPermissions
getDefaultGoalChooserBuilder, getDefaultProfile, getInternalClassDirectory, getInternalClasslistFilename, getSelectedGoalChooserBuilder, getStandardRules, getStrategyFactory, getTermLabelManager, lookupGC, setDefaultProfile, setSelectedGoalChooserBuilder, supportedGoalChoosers, supportedStrategies, supportsStrategyFactory
public static final java.lang.String NAME
private static final StrategyFactory SYMBOLIC_EXECUTION_FACTORY
StrategyFactory
of the SymbolicExecutionStrategy
.private final java.lang.Boolean truthValueEvaluationEnabled
true
truth value evaluation is enabled, false
truth value evaluation is disabled.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 Thread
s (not the UI Thread
).
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 Thread
s (not the UI Thread
).
public SymbolicExecutionJavaProfile(boolean predicateEvaluationEnabled)
predicateEvaluationEnabled
- true
predicate evaluation is enabled, false
predicate evaluation is disabled.protected ImmutableSet<GoalChooserBuilder> computeSupportedGoalChooserBuilder()
computeSupportedGoalChooserBuilder
in class AbstractProfile
protected void initTermLabelManager()
TermLabelManager
.initTermLabelManager
in class AbstractProfile
protected ImmutableList<TermLabelManager.TermLabelConfiguration> computeTermLabelConfiguration()
TermLabelManager.TermLabelConfiguration
to use in this Profile
.computeTermLabelConfiguration
in class JavaProfile
TermLabelManager.TermLabelConfiguration
to use in this Profile
.public static ImmutableList<TermLabelManager.TermLabelConfiguration> getSymbolicExecutionTermLabelConfigurations(boolean predicateEvaluationEnabled)
TermLabelFactory
instances used for symbolic execution.predicateEvaluationEnabled
- true
predicate evaluation is enabled, false
predicate evaluation is disabled.TermLabelFactory
instances used for symbolic execution.protected ImmutableSet<StrategyFactory> getStrategyFactories()
getStrategyFactories
in class JavaProfile
protected ImmutableList<BuiltInRule> initBuiltInRules()
initBuiltInRules
in class JavaProfile
public java.lang.String name()
name
in interface Profile
name
in class JavaProfile
public boolean isPredicateEvaluationEnabled()
true
predicate evaluation is enabled, false
predicate evaluation is disabled.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 Thread
s (not the UI Thread
).
Thread
of the user interface.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 Thread
s (not the UI Thread
).
truthValueEvaluationEnabled
- true
truth value evaluation is enabled, false
truth value evaluation is disabled.Thread
of the user interface.public static boolean isTruthValueTracingEnabled(Proof proof)
Proof
.proof
- The Proof
to check.true
truth value evaluation is enabled, false
truth value evaluation is disabled.public static boolean isTruthValueEvaluationEnabled(InitConfig initConfig)
InitConfig
.initConfig
- The InitConfig
to check.true
truth value evaluation is enabled, false
truth value evaluation is disabled.