cprover
nondet_static.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Nondeterministic initialization of certain global scope
4  variables
5 
6 Author: Daniel Kroening, Michael Tautschnig
7 
8 Date: November 2011
9 
10 \*******************************************************************/
11 
14 
15 #ifndef CPROVER_GOTO_INSTRUMENT_NONDET_STATIC_H
16 #define CPROVER_GOTO_INSTRUMENT_NONDET_STATIC_H
17 
18 class goto_modelt;
19 class namespacet;
20 class goto_functionst;
21 
22 void nondet_static(
23  const namespacet &ns,
24  goto_functionst &goto_functions);
25 
27 
28 #endif // CPROVER_GOTO_INSTRUMENT_NONDET_STATIC_H
TO_BE_DOCUMENTED.
Definition: namespace.h:74
void nondet_static(const namespacet &ns, goto_functionst &goto_functions)