cprover
nondet_static.h
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: Nondeterministically initializes global scope variables, except for
4
constants (such as string literals, final fields) and internal variables
5
(such as CPROVER and symex variables, language specific internal
6
variables).
7
8
Author: Daniel Kroening, Michael Tautschnig
9
10
Date: November 2011
11
12
\*******************************************************************/
13
19
20
#ifndef CPROVER_GOTO_INSTRUMENT_NONDET_STATIC_H
21
#define CPROVER_GOTO_INSTRUMENT_NONDET_STATIC_H
22
23
#include <
util/options.h
>
24
25
class
goto_modelt
;
26
class
namespacet
;
27
class
goto_functionst
;
28
class
symbol_exprt
;
29
30
bool
is_nondet_initializable_static
(
31
const
symbol_exprt
&symbol_expr,
32
const
namespacet
&ns);
33
34
void
nondet_static
(
35
const
namespacet
&ns,
36
goto_functionst
&goto_functions);
37
38
void
nondet_static
(
goto_modelt
&);
39
40
void
nondet_static
(
goto_modelt
&,
const
optionst::value_listt
&);
41
42
#endif // CPROVER_GOTO_INSTRUMENT_NONDET_STATIC_H
is_nondet_initializable_static
bool is_nondet_initializable_static(const symbol_exprt &symbol_expr, const namespacet &ns)
See the return.
Definition:
nondet_static.cpp:33
goto_modelt
Definition:
goto_model.h:26
options.h
Options.
optionst::value_listt
std::list< std::string > value_listt
Definition:
options.h:25
symbol_exprt
Expression to hold a symbol (variable)
Definition:
std_expr.h:82
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition:
namespace.h:92
nondet_static
void nondet_static(const namespacet &ns, goto_functionst &goto_functions)
Nondeterministically initializes global scope variables in CPROVER_initialize function.
Definition:
nondet_static.cpp:128
goto_functionst
A collection of goto functions.
Definition:
goto_functions.h:23
goto-instrument
nondet_static.h
Generated by
1.8.20