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 <set>
24#include <string>
25
26class goto_modelt;
27class namespacet;
28class goto_functionst;
29class symbol_exprt;
30
31bool is_nondet_initializable_static(
32 const symbol_exprt &symbol_expr,
33 const namespacet &ns);
34
35void nondet_static(goto_modelt &);
36
37void nondet_static(goto_modelt &, const std::set<std::string> &);
38
39void nondet_static_matching(goto_modelt &, const std::string &);
40
41#endif // CPROVER_GOTO_INSTRUMENT_NONDET_STATIC_H
goto_functionst
A collection of goto functions.
Definition goto_functions.h:25
goto_modelt
Definition goto_model.h:27
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
symbol_exprt
Expression to hold a symbol (variable).
Definition std_expr.h:132
is_nondet_initializable_static
bool is_nondet_initializable_static(const symbol_exprt &symbol_expr, const namespacet &ns)
See the return.
Definition nondet_static.cpp:36
nondet_static_matching
void nondet_static_matching(goto_modelt &, const std::string &)
Nondeterministically initializes global scope variables that match the given regex.
Definition nondet_static.cpp:203
nondet_static
void nondet_static(goto_modelt &)
First main entry point of the module.
Definition nondet_static.cpp:131