cprover
nondet_volatile.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Volatile Variables
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_INSTRUMENT_NONDET_VOLATILE_H
13 #define CPROVER_GOTO_INSTRUMENT_NONDET_VOLATILE_H
14 
16 
17 class cmdlinet;
18 class optionst;
19 
20 // clang-format off
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"
24 
25 #define OPT_NONDET_VOLATILE \
26  "(" NONDET_VOLATILE_OPT ")" \
27  "(" NONDET_VOLATILE_VARIABLE_OPT "):" \
28  "(" NONDET_VOLATILE_MODEL_OPT "):"
29 
30 #define HELP_NONDET_VOLATILE \
31  help_entry( \
32  "--" NONDET_VOLATILE_OPT, \
33  "makes reads from volatile variables non-deterministic") << \
34  help_entry( \
35  "--" NONDET_VOLATILE_VARIABLE_OPT " <variable>", \
36  "makes reads from given volatile variable non-deterministic") << \
37  help_entry( \
38  "--" NONDET_VOLATILE_MODEL_OPT " <variable>:<model>", \
39  "models reads from given volatile variable by a call to the given model")
40 // clang-format on
41 
42 void parse_nondet_volatile_options(const cmdlinet &cmdline, optionst &options);
43 
48 void nondet_volatile(goto_modelt &goto_model, const optionst &options);
49 
56  goto_modelt &goto_model,
57  std::function<bool(const exprt &)> should_havoc = [](const exprt &) {
58  return true;
59  });
60 
61 #endif // CPROVER_GOTO_INSTRUMENT_NONDET_VOLATILE_H
optionst
Definition: options.h:23
parse_nondet_volatile_options
void parse_nondet_volatile_options(const cmdlinet &cmdline, optionst &options)
Definition: nondet_volatile.cpp:406
goto_model.h
Symbol Table + CFG.
exprt
Base class for all expressions.
Definition: expr.h:53
goto_modelt
Definition: goto_model.h:26
cmdlinet
Definition: cmdline.h:21
nondet_volatile
void nondet_volatile(goto_modelt &goto_model, const optionst &options)
Havoc reads from volatile expressions, if enabled in the options.
Definition: nondet_volatile.cpp:452