cprover
Loading...
Searching...
No Matches
nondet_static.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: 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
8Author: Daniel Kroening, Michael Tautschnig
9
10Date: 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
25class goto_modelt;
26class namespacet;
27class goto_functionst;
28class symbol_exprt;
29
31 const symbol_exprt &symbol_expr,
32 const namespacet &ns);
33
34void nondet_static(
35 const namespacet &ns,
36 goto_functionst &goto_functions);
37
39
41
42#endif // CPROVER_GOTO_INSTRUMENT_NONDET_STATIC_H
A collection of goto functions.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
std::list< std::string > value_listt
Definition: options.h:25
Expression to hold a symbol (variable)
Definition: std_expr.h:80
bool is_nondet_initializable_static(const symbol_exprt &symbol_expr, const namespacet &ns)
See the return.
void nondet_static(const namespacet &ns, goto_functionst &goto_functions)
Nondeterministically initializes global scope variables in CPROVER_initialize function.
Options.