20 #ifndef CPROVER_GOTO_INSTRUMENT_NONDET_STATIC_H 21 #define CPROVER_GOTO_INSTRUMENT_NONDET_STATIC_H 38 #endif // CPROVER_GOTO_INSTRUMENT_NONDET_STATIC_H
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
void nondet_static(const namespacet &ns, goto_functionst &goto_functions)
Nondeterministically initializes global scope variables in CPROVER_initialize function.
A collection of goto functions.
bool is_nondet_initializable_static(const symbol_exprt &symbol_expr, const namespacet &ns)
See the return.
Expression to hold a symbol (variable)