cprover
Loading...
Searching...
No Matches
nondet_volatile.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Volatile Variables
4
5Author: 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
17class cmdlinet;
18class exprt;
19class goto_modelt;
20class 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 help_entry( \
34 "--" NONDET_VOLATILE_OPT, \
35 "makes reads from volatile variables non-deterministic") << \
36 help_entry( \
37 "--" NONDET_VOLATILE_VARIABLE_OPT " <variable>", \
38 "makes reads from given volatile variable non-deterministic") << \
39 help_entry( \
40 "--" NONDET_VOLATILE_MODEL_OPT " <variable>:<model>", \
41 "models reads from given volatile variable by a call to the given model")
42// clang-format on
43
44void parse_nondet_volatile_options(const cmdlinet &cmdline, optionst &options);
45
50void nondet_volatile(goto_modelt &goto_model, const optionst &options);
51
58 goto_modelt &goto_model,
59 std::function<bool(const exprt &)> should_havoc = [](const exprt &) {
60 return true;
61 });
62
63#endif // CPROVER_GOTO_INSTRUMENT_NONDET_VOLATILE_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Base class for all expressions.
Definition expr.h:54
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.