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 | Constructor and Description |
---|---|
private |
SymbolicExecutionStrategy(Proof proof,
StrategyProperties sp)
Constructor.
|
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
private SymbolicExecutionStrategy(Proof proof, StrategyProperties sp)
proof
- The proof.sp
- The StrategyProperties
to use.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.