CBMC
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 
15 #include <functional>
16 
17 class cmdlinet;
18 class exprt;
19 class goto_modelt;
20 class optionst;
21 
22 // clang-format off
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"
26 
27 #define OPT_NONDET_VOLATILE \
28  "(" NONDET_VOLATILE_OPT ")" \
29  "(" NONDET_VOLATILE_VARIABLE_OPT "):" \
30  "(" NONDET_VOLATILE_MODEL_OPT "):"
31 
32 #define HELP_NONDET_VOLATILE \
33  " {y--" NONDET_VOLATILE_OPT "} \t " \
34  "makes reads from volatile variables non-deterministic\n" \
35  " {y--" NONDET_VOLATILE_VARIABLE_OPT "} {uvariable} \t " \
36  "makes reads from given volatile variable non-deterministic\n" \
37  " {y--" NONDET_VOLATILE_MODEL_OPT "} {uvariable}:{umodel} \t " \
38  "models reads from given volatile variable by a call to the given model\n" \
39 // clang-format on
40 
41 void parse_nondet_volatile_options(const cmdlinet &cmdline, optionst &options);
42 
47 void nondet_volatile(goto_modelt &goto_model, const optionst &options);
48 
55  goto_modelt &goto_model,
56  std::function<bool(const exprt &)> should_havoc = [](const exprt &) {
57  return true;
58  });
59 
60 #endif // CPROVER_GOTO_INSTRUMENT_NONDET_VOLATILE_H
Base class for all expressions.
Definition: expr.h:56
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.