CBMC
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 <set>
24 #include <string>
25 
26 class goto_modelt;
27 class namespacet;
28 class goto_functionst;
29 class symbol_exprt;
30 
31 bool is_nondet_initializable_static(
32  const symbol_exprt &symbol_expr,
33  const namespacet &ns);
34 
35 void nondet_static(
36  const namespacet &ns,
37  goto_functionst &goto_functions);
38 
39 void nondet_static(goto_modelt &);
40 
41 void nondet_static(goto_modelt &, const std::set<std::string> &);
42 
43 #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:34
goto_modelt
Definition: goto_model.h:25
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:112
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:90
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:124
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:24