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
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?