public class SymbolicExecutionStrategy extends JavaCardDLStrategy
Strategy
to use for symbolic execution.Modifier and Type | Class and Description |
---|---|
static class |
SymbolicExecutionStrategy.Factory
The
StrategyFactory to create instances of SymbolicExecutionStrategy . |
Modifier and Type | Field and Description |
---|---|
static IDefaultStrategyPropertiesFactory |
DEFAULT_FACTORY
The default factory.
|
static Name |
name
|
JAVA_CARD_DL_STRATEGY, strategyProperties
Modifier and Type | Method and Description |
---|---|
static StrategyProperties |
getSymbolicExecutionStrategyProperties(boolean quantifierInstantiationWithSplitting,
boolean methodTreatmentContract,
boolean loopTreatmentInvariant,
boolean blockTreatmentContract,
boolean nonExecutionBranchHidingSideProofs,
boolean aliasChecks)
Returns the default
StrategyProperties of symbolic execution. |
protected Feature |
modalitySideProofFeature()
Computes the cost
Feature for the ModalitySideProofRule . |
Name |
name()
returns the name of this element
|
protected Feature |
querySideProofFeature()
Computes the cost
Feature for the QuerySideProofRule . |
protected Feature |
setupApprovalF() |
protected Feature |
setupGlobalF(Feature dispatcher) |
arithDefOps, computeCost, getCostComputationDispatcher, getInstantiationDispatcher, getServices, instantiateApp, isApprovedApp, isStopAtFirstNonCloseableGoal
bindRuleSet, bindRuleSet, bindRuleSet, bindRuleSet, clearRuleSetBindings, clearRuleSetBindings, disableInstantiate, enableInstantiate, forEach, getFilterFor, getHeuristic, getProof, ifHeuristics, ifHeuristics, ifHeuristics, instantiate, instantiate, instantiateApp, instantiateTriggeredVariable, oneOf, oneOf
add, add, add, add, add, any, applyTF, applyTF, applyTFNonStrict, applyTFNonStrict, atomSmallerThan, blockContractExternalFeature, blockContractInternalFeature, c, contains, countOccurrences, eq, eq, eq, extendsTrans, ifZero, ifZero, ifZero, ifZero, implicitCastNecessary, inftyConst, inftyTermConst, instOf, instOfNonStrict, instOfTriggerVariable, isInstantiated, isSubSortFeature, isTriggerVariableInstantiated, leq, less, let, literalsSmallerThan, longConst, longTermConst, loopContractApplyHead, loopContractExternalFeature, loopContractInternalFeature, loopInvFeature, mergeRuleFeature, methodSpecFeature, monSmallerThan, not, not, op, opSub, opSub, opTerm, opTerm, opTerm, or, or, or, or, or, println, querySpecFeature, rec, sequentContainsNoPrograms, sub, sub, sub, subAt, sum, termSmallerThan
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
updateStrategySettings
public static final Name name
public static IDefaultStrategyPropertiesFactory DEFAULT_FACTORY
protected Feature setupApprovalF()
setupApprovalF
in class JavaCardDLStrategy
protected Feature setupGlobalF(Feature dispatcher)
setupGlobalF
in class JavaCardDLStrategy
protected Feature modalitySideProofFeature()
Feature
for the ModalitySideProofRule
.Feature
for the ModalitySideProofRule
.protected Feature querySideProofFeature()
Feature
for the QuerySideProofRule
.Feature
for the QuerySideProofRule
.public Name name()
name
in interface Named
name
in class JavaCardDLStrategy
public static StrategyProperties getSymbolicExecutionStrategyProperties(boolean quantifierInstantiationWithSplitting, boolean methodTreatmentContract, boolean loopTreatmentInvariant, boolean blockTreatmentContract, boolean nonExecutionBranchHidingSideProofs, boolean aliasChecks)
StrategyProperties
of symbolic execution.quantifierInstantiationWithSplitting
- Instantiate quantifiers?methodTreatmentContract
- Use method contracts or inline method bodies otherwise?loopTreatmentInvariant
- Use loop invariants or unrole loops otherwise?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?StrategyProperties
for symbolic execution.Copyright © 2003-2019 The KeY-Project.