cprover
Loading...
Searching...
No Matches
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
54
void
nondet_volatile
(
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
cmdlinet
Definition
cmdline.h:21
exprt
Base class for all expressions.
Definition
expr.h:56
goto_modelt
Definition
goto_model.h:27
optionst
Definition
options.h:23
parse_nondet_volatile_options
void parse_nondet_volatile_options(const cmdlinet &cmdline, optionst &options)
Definition
nondet_volatile.cpp:409
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:455
goto-instrument
nondet_volatile.h
Generated by
1.11.0