public final class StrategyProperties
extends java.util.Properties
Modifier and Type | Field and Description |
---|---|
static java.lang.String |
AUTO_INDUCTION_LEMMA_ON |
static java.lang.String |
AUTO_INDUCTION_OFF |
static java.lang.String |
AUTO_INDUCTION_ON |
static java.lang.String |
AUTO_INDUCTION_OPTIONS_KEY |
static java.lang.String |
AUTO_INDUCTION_RESTRICTED |
static java.lang.String |
BLOCK_CONTRACT_EXTERNAL |
static java.lang.String |
BLOCK_CONTRACT_INTERNAL |
static java.lang.String |
BLOCK_EXPAND |
static java.lang.String |
BLOCK_NONE |
static java.lang.String |
BLOCK_OPTIONS_KEY |
static java.lang.String |
CLASS_AXIOM_DELAYED |
static java.lang.String |
CLASS_AXIOM_FREE |
static java.lang.String |
CLASS_AXIOM_OFF |
static java.lang.String |
CLASS_AXIOM_OPTIONS_KEY |
private static java.util.Properties |
DEFAULT_MAP |
static java.lang.String |
DEP_OFF |
static java.lang.String |
DEP_ON |
static java.lang.String |
DEP_OPTIONS_KEY |
static java.lang.String |
INF_FLOW_CHECK_FALSE |
static java.lang.String |
INF_FLOW_CHECK_PROPERTY |
static java.lang.String |
INF_FLOW_CHECK_TRUE |
static java.lang.String |
LOOP_EXPAND |
static java.lang.String |
LOOP_EXPAND_BOUNDED |
static java.lang.String |
LOOP_INVARIANT |
static java.lang.String |
LOOP_NONE |
static java.lang.String |
LOOP_OPTIONS_KEY |
static java.lang.String |
LOOP_SCOPE_INVARIANT |
static java.lang.String |
METHOD_CONTRACT |
static java.lang.String |
METHOD_EXPAND |
static java.lang.String |
METHOD_NONE |
static java.lang.String |
METHOD_OPTIONS_KEY |
static java.lang.String |
MPS_MERGE |
static java.lang.String |
MPS_NONE |
static java.lang.String |
MPS_OPTIONS_KEY |
static java.lang.String |
MPS_SKIP |
static java.lang.String |
NON_LIN_ARITH_COMPLETION |
static java.lang.String |
NON_LIN_ARITH_DEF_OPS |
static java.lang.String |
NON_LIN_ARITH_NONE |
static java.lang.String |
NON_LIN_ARITH_OPTIONS_KEY |
static java.lang.String |
OSS_OFF |
static java.lang.String |
OSS_ON |
static java.lang.String |
OSS_OPTIONS_KEY |
static java.lang.String |
QUANTIFIERS_INSTANTIATE |
static java.lang.String |
QUANTIFIERS_NON_SPLITTING |
static java.lang.String |
QUANTIFIERS_NON_SPLITTING_WITH_PROGS |
static java.lang.String |
QUANTIFIERS_NONE |
static java.lang.String |
QUANTIFIERS_OPTIONS_KEY |
static java.lang.String |
QUERY_OFF |
static java.lang.String |
QUERY_ON |
static java.lang.String |
QUERY_OPTIONS_KEY |
static java.lang.String |
QUERY_RESTRICTED |
static java.lang.String |
QUERYAXIOM_OFF |
static java.lang.String |
QUERYAXIOM_ON |
static java.lang.String |
QUERYAXIOM_OPTIONS_KEY |
private static long |
serialVersionUID |
static java.lang.String |
SPLITTING_DELAYED |
static java.lang.String |
SPLITTING_NORMAL |
static java.lang.String |
SPLITTING_OFF |
static java.lang.String |
SPLITTING_OPTIONS_KEY |
static java.lang.String |
STOPMODE_DEFAULT |
static java.lang.String |
STOPMODE_NONCLOSE |
static java.lang.String |
STOPMODE_OPTIONS_KEY |
private static java.lang.String |
STRATEGY_PROPERTY
Section key for storage file to identify strategy settings
|
private static java.lang.String[] |
STRING_POOL |
static java.lang.String |
SYMBOLIC_EXECUTION_ALIAS_CHECK_IMMEDIATELY
Value of key
SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY in
StrategyProperties to enable immediately alias checks in a
SymbolicExecutionStrategy . |
static java.lang.String |
SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER
Value of key
SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY in
StrategyProperties to disable alias checks in a
SymbolicExecutionStrategy . |
static java.lang.String |
SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY
Key used in
StrategyProperties to configure alias checks in a
SymbolicExecutionStrategy}. |
static java.lang.String |
SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF
Value of key
SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY
in StrategyProperties to disable branch avoiding caused by
modalities not part of main execution in a
SymbolicExecutionStrategy . |
static java.lang.String |
SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY
Key used in
StrategyProperties to avoid branches caused by
modalities not part of main execution branch in a
SymbolicExecutionStrategy . |
static java.lang.String |
SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_SIDE_PROOF
Value of key
SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY
in StrategyProperties to avoid branches caused by modalities not
part of main execution by using site proofs in a
SymbolicExecutionStrategy . |
static java.lang.String |
USER_TACLETS_HIGH |
static java.lang.String |
USER_TACLETS_LOW |
static int |
USER_TACLETS_NUM |
static java.lang.String |
USER_TACLETS_OFF |
private static java.lang.String |
USER_TACLETS_OPTIONS_KEY_BASE |
static java.lang.String |
VBT_MODEL_GEN |
static java.lang.String |
VBT_PHASE |
static java.lang.String |
VBT_QUAN_INST |
static java.lang.String |
VBT_SYM_EX |
Constructor and Description |
---|
StrategyProperties() |
Modifier and Type | Method and Description |
---|---|
java.lang.Object |
clone() |
static java.lang.String |
getDefaultProperty(java.lang.String key) |
java.lang.String |
getProperty(java.lang.String key) |
private static java.lang.String |
getUniqueString(java.lang.String in) |
boolean |
isDefault() |
static StrategyProperties |
read(java.util.Properties p) |
private static java.lang.Object |
readSingleOption(java.util.Properties p,
java.lang.String key) |
static void |
setDefaultStrategyProperties(StrategyProperties sp,
boolean quantifierInstantiationWithSplitting,
boolean methodTreatmentContract,
boolean loopTreatmentInvariant,
boolean blockTreatmentContract,
boolean nonExecutionBranchHidingSideProofs,
boolean aliasChecks)
Sets the default settings for symbolic execution on the given
StrategyProperties . |
static java.lang.String |
userTacletsOptionsKey(int i) |
void |
write(java.util.Properties p) |
getProperty, list, list, load, load, loadFromXML, propertyNames, save, setProperty, store, store, storeToXML, storeToXML, stringPropertyNames
clear, compute, computeIfAbsent, computeIfPresent, contains, containsKey, containsValue, elements, entrySet, equals, forEach, get, getOrDefault, hashCode, isEmpty, keys, keySet, merge, put, putAll, putIfAbsent, rehash, remove, remove, replace, replace, replaceAll, size, toString, values
public static final java.lang.String INF_FLOW_CHECK_PROPERTY
public static final java.lang.String INF_FLOW_CHECK_TRUE
public static final java.lang.String INF_FLOW_CHECK_FALSE
public static final java.lang.String STOPMODE_OPTIONS_KEY
public static final java.lang.String STOPMODE_DEFAULT
public static final java.lang.String STOPMODE_NONCLOSE
public static final java.lang.String SPLITTING_OPTIONS_KEY
public static final java.lang.String SPLITTING_NORMAL
public static final java.lang.String SPLITTING_OFF
public static final java.lang.String SPLITTING_DELAYED
public static final java.lang.String LOOP_OPTIONS_KEY
public static final java.lang.String LOOP_EXPAND
public static final java.lang.String LOOP_EXPAND_BOUNDED
public static final java.lang.String LOOP_INVARIANT
public static final java.lang.String LOOP_SCOPE_INVARIANT
public static final java.lang.String LOOP_NONE
public static final java.lang.String BLOCK_OPTIONS_KEY
public static final java.lang.String BLOCK_CONTRACT_INTERNAL
public static final java.lang.String BLOCK_CONTRACT_EXTERNAL
public static final java.lang.String BLOCK_EXPAND
public static final java.lang.String BLOCK_NONE
public static final java.lang.String METHOD_OPTIONS_KEY
public static final java.lang.String METHOD_EXPAND
public static final java.lang.String METHOD_CONTRACT
public static final java.lang.String METHOD_NONE
public static final java.lang.String MPS_OPTIONS_KEY
public static final java.lang.String MPS_SKIP
public static final java.lang.String MPS_MERGE
public static final java.lang.String MPS_NONE
public static final java.lang.String DEP_OPTIONS_KEY
public static final java.lang.String DEP_ON
public static final java.lang.String DEP_OFF
public static final java.lang.String QUERY_OPTIONS_KEY
public static final java.lang.String QUERY_ON
public static final java.lang.String QUERY_RESTRICTED
public static final java.lang.String QUERY_OFF
public static final java.lang.String QUERYAXIOM_OPTIONS_KEY
public static final java.lang.String QUERYAXIOM_ON
public static final java.lang.String QUERYAXIOM_OFF
public static final java.lang.String NON_LIN_ARITH_OPTIONS_KEY
public static final java.lang.String NON_LIN_ARITH_NONE
public static final java.lang.String NON_LIN_ARITH_DEF_OPS
public static final java.lang.String NON_LIN_ARITH_COMPLETION
public static final java.lang.String OSS_OPTIONS_KEY
public static final java.lang.String OSS_ON
public static final java.lang.String OSS_OFF
public static final java.lang.String QUANTIFIERS_OPTIONS_KEY
public static final java.lang.String QUANTIFIERS_NONE
public static final java.lang.String QUANTIFIERS_NON_SPLITTING
public static final java.lang.String QUANTIFIERS_NON_SPLITTING_WITH_PROGS
public static final java.lang.String QUANTIFIERS_INSTANTIATE
public static final java.lang.String VBT_PHASE
public static final java.lang.String VBT_SYM_EX
public static final java.lang.String VBT_QUAN_INST
public static final java.lang.String VBT_MODEL_GEN
public static final java.lang.String CLASS_AXIOM_OPTIONS_KEY
public static final java.lang.String CLASS_AXIOM_OFF
public static final java.lang.String CLASS_AXIOM_DELAYED
public static final java.lang.String CLASS_AXIOM_FREE
public static final java.lang.String AUTO_INDUCTION_OPTIONS_KEY
public static final java.lang.String AUTO_INDUCTION_OFF
public static final java.lang.String AUTO_INDUCTION_RESTRICTED
public static final java.lang.String AUTO_INDUCTION_ON
public static final java.lang.String AUTO_INDUCTION_LEMMA_ON
public static final int USER_TACLETS_NUM
public static final java.lang.String USER_TACLETS_OFF
public static final java.lang.String USER_TACLETS_LOW
public static final java.lang.String USER_TACLETS_HIGH
public static final java.lang.String SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY
StrategyProperties
to configure alias checks in a
SymbolicExecutionStrategy}.public static final java.lang.String SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER
SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY
in
StrategyProperties
to disable alias checks in a
SymbolicExecutionStrategy
.public static final java.lang.String SYMBOLIC_EXECUTION_ALIAS_CHECK_IMMEDIATELY
SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY
in
StrategyProperties
to enable immediately alias checks in a
SymbolicExecutionStrategy
.public static final java.lang.String SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY
StrategyProperties
to avoid branches caused by
modalities not part of main execution branch in a
SymbolicExecutionStrategy
.public static final java.lang.String SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF
SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY
in StrategyProperties
to disable branch avoiding caused by
modalities not part of main execution in a
SymbolicExecutionStrategy
.public static final java.lang.String SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_SIDE_PROOF
SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY
in StrategyProperties
to avoid branches caused by modalities not
part of main execution by using site proofs in a
SymbolicExecutionStrategy
.private static final long serialVersionUID
private static final java.lang.String STRATEGY_PROPERTY
private static final java.lang.String USER_TACLETS_OPTIONS_KEY_BASE
private static final java.lang.String[] STRING_POOL
private static final java.util.Properties DEFAULT_MAP
public static java.lang.String userTacletsOptionsKey(int i)
public static java.lang.String getDefaultProperty(java.lang.String key)
public static StrategyProperties read(java.util.Properties p)
public static void setDefaultStrategyProperties(StrategyProperties sp, boolean quantifierInstantiationWithSplitting, boolean methodTreatmentContract, boolean loopTreatmentInvariant, boolean blockTreatmentContract, boolean nonExecutionBranchHidingSideProofs, boolean aliasChecks)
StrategyProperties
.sp
- The StrategyProperties
to modify.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?private static java.lang.Object readSingleOption(java.util.Properties p, java.lang.String key)
p
- private static final java.lang.String getUniqueString(java.lang.String in)
in
- A keyword from the strategy properties. It must be registered
in stringPool
.public java.lang.String getProperty(java.lang.String key)
getProperty
in class java.util.Properties
public void write(java.util.Properties p)
public java.lang.Object clone()
clone
in class java.util.Hashtable<java.lang.Object,java.lang.Object>
public boolean isDefault()