12 #ifndef CPROVER_GOTO_INSTRUMENT_NONDET_VOLATILE_H
13 #define CPROVER_GOTO_INSTRUMENT_NONDET_VOLATILE_H
23 #define NONDET_VOLATILE_OPT "nondet-volatile"
24 #define NONDET_VOLATILE_VARIABLE_OPT "nondet-volatile-variable"
25 #define NONDET_VOLATILE_MODEL_OPT "nondet-volatile-model"
27 #define OPT_NONDET_VOLATILE \
28 "(" NONDET_VOLATILE_OPT ")" \
29 "(" NONDET_VOLATILE_VARIABLE_OPT "):" \
30 "(" NONDET_VOLATILE_MODEL_OPT "):"
32 #define HELP_NONDET_VOLATILE \
34 "--" NONDET_VOLATILE_OPT, \
35 "makes reads from volatile variables non-deterministic") << \
37 "--" NONDET_VOLATILE_VARIABLE_OPT " <variable>", \
38 "makes reads from given volatile variable non-deterministic") << \
40 "--" NONDET_VOLATILE_MODEL_OPT " <variable>:<model>", \
41 "models reads from given volatile variable by a call to the given model")
59 std::function<
bool(
const exprt &)> should_havoc = [](
const exprt &) {
Base class for all expressions.
void parse_nondet_volatile_options(const cmdlinet &cmdline, optionst &options)
void nondet_volatile(goto_modelt &goto_model, const optionst &options)
Havoc reads from volatile expressions, if enabled in the options.