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
15
#include <
goto-programs/goto_model.h
>
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
55
void
nondet_volatile
(
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
goto-instrument
nondet_volatile.h
Generated by
1.8.20