12 #ifndef CPROVER_GOTO_INSTRUMENT_NONDET_VOLATILE_H
13 #define CPROVER_GOTO_INSTRUMENT_NONDET_VOLATILE_H
21 #define NONDET_VOLATILE_OPT "nondet-volatile"
22 #define NONDET_VOLATILE_VARIABLE_OPT "nondet-volatile-variable"
23 #define NONDET_VOLATILE_MODEL_OPT "nondet-volatile-model"
25 #define OPT_NONDET_VOLATILE \
26 "(" NONDET_VOLATILE_OPT ")" \
27 "(" NONDET_VOLATILE_VARIABLE_OPT "):" \
28 "(" NONDET_VOLATILE_MODEL_OPT "):"
30 #define HELP_NONDET_VOLATILE \
32 "--" NONDET_VOLATILE_OPT, \
33 "makes reads from volatile variables non-deterministic") << \
35 "--" NONDET_VOLATILE_VARIABLE_OPT " <variable>", \
36 "makes reads from given volatile variable non-deterministic") << \
38 "--" NONDET_VOLATILE_MODEL_OPT " <variable>:<model>", \
39 "models reads from given volatile variable by a call to the given model")
57 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.