public final class StrategyProperties extends Properties
defaults
Constructor and Description |
---|
StrategyProperties() |
Modifier and Type | Method and Description |
---|---|
Object |
clone() |
static String |
getDefaultProperty(String key) |
String |
getProperty(String key) |
private static String |
getUniqueString(String in) |
boolean |
isDefault() |
static StrategyProperties |
read(Properties p) |
private static Object |
readSingleOption(Properties p,
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 String |
USER_TACLETS_OPTIONS_KEY(int i) |
void |
write(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
private static final long serialVersionUID
public static final String INF_FLOW_CHECK_PROPERTY
public static final String INF_FLOW_CHECK_TRUE
public static final String INF_FLOW_CHECK_FALSE
private static final String STRATEGY_PROPERTY
public static final String STOPMODE_OPTIONS_KEY
public static final String STOPMODE_DEFAULT
public static final String STOPMODE_NONCLOSE
public static final String SPLITTING_OPTIONS_KEY
public static final String SPLITTING_NORMAL
public static final String SPLITTING_OFF
public static final String SPLITTING_DELAYED
public static final String LOOP_OPTIONS_KEY
public static final String LOOP_EXPAND
public static final String LOOP_EXPAND_BOUNDED
public static final String LOOP_INVARIANT
public static final String LOOP_NONE
public static final String BLOCK_OPTIONS_KEY
public static final String BLOCK_CONTRACT
public static final String BLOCK_EXPAND
public static final String BLOCK_NONE
public static final String METHOD_OPTIONS_KEY
public static final String METHOD_EXPAND
public static final String METHOD_CONTRACT
public static final String METHOD_NONE
public static final String DEP_OPTIONS_KEY
public static final String DEP_ON
public static final String DEP_OFF
public static final String QUERY_OPTIONS_KEY
public static final String QUERY_ON
public static final String QUERY_RESTRICTED
public static final String QUERY_OFF
public static final String QUERYAXIOM_OPTIONS_KEY
public static final String QUERYAXIOM_ON
public static final String QUERYAXIOM_OFF
public static final String NON_LIN_ARITH_OPTIONS_KEY
public static final String NON_LIN_ARITH_NONE
public static final String NON_LIN_ARITH_DEF_OPS
public static final String NON_LIN_ARITH_COMPLETION
public static final String QUANTIFIERS_OPTIONS_KEY
public static final String QUANTIFIERS_NONE
public static final String QUANTIFIERS_NON_SPLITTING
public static final String QUANTIFIERS_NON_SPLITTING_WITH_PROGS
public static final String QUANTIFIERS_INSTANTIATE
public static final String VBT_PHASE
public static final String VBT_SYM_EX
public static final String VBT_QUAN_INST
public static final String VBT_MODEL_GEN
public static final String CLASS_AXIOM_OPTIONS_KEY
public static final String CLASS_AXIOM_OFF
public static final String CLASS_AXIOM_DELAYED
public static final String CLASS_AXIOM_FREE
public static final String AUTO_INDUCTION_OPTIONS_KEY
public static final String AUTO_INDUCTION_OFF
public static final String AUTO_INDUCTION_RESTRICTED
public static final String AUTO_INDUCTION_ON
public static final String AUTO_INDUCTION_LEMMA_ON
public static final int USER_TACLETS_NUM
private static final String USER_TACLETS_OPTIONS_KEY_BASE
public static final String USER_TACLETS_OFF
public static final String USER_TACLETS_LOW
public static final String USER_TACLETS_HIGH
public static final String SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY
StrategyProperties
to configure alias checks in a SymbolicExecutionStrategy}.public static final String SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER
SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY
in StrategyProperties
to disable alias checks in a SymbolicExecutionStrategy
.public static final 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 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 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 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 String[] stringPool
private static final Properties defaultMap
public static String USER_TACLETS_OPTIONS_KEY(int i)
public String getProperty(String key)
getProperty
in class Properties
public static StrategyProperties read(Properties p)
private static Object readSingleOption(Properties p, String key)
p
- public void write(Properties p)
public boolean isDefault()
private static final String getUniqueString(String in)
in
- A keyword from the strategy properties. It must be registered in stringPool<\code>.
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?