cprover
|
Nondeterministic initialization of certain global scope variables. More...
#include "nondet_static.h"
#include <util/namespace.h>
#include <util/std_expr.h>
#include <util/cprover_prefix.h>
#include <util/prefix.h>
#include <goto-programs/goto_functions.h>
Go to the source code of this file.
Functions | |
void | nondet_static (const namespacet &ns, goto_functionst &goto_functions, const irep_idt &fct_name) |
void | nondet_static (const namespacet &ns, goto_functionst &goto_functions) |
Nondeterministic initialization of certain global scope variables.
Definition in file nondet_static.cpp.
void nondet_static | ( | const namespacet & | ns, |
goto_functionst & | goto_functions, | ||
const irep_idt & | fct_name | ||
) |
Definition at line 24 of file nondet_static.cpp.
References CPROVER_PREFIX, Forall_goto_program_instructions, code_function_callt::function(), goto_functions_templatet< bodyT >::function_map, irept::get_bool(), symbol_exprt::get_identifier(), has_prefix(), id2string(), code_assignt::lhs(), namespacet::lookup(), to_code_assign(), to_code_function_call(), to_symbol_expr(), and exprt::type().
Referenced by goto_instrument_parse_optionst::instrument_goto_program(), nondet_static(), and cbmc_parse_optionst::process_goto_program().
void nondet_static | ( | const namespacet & | ns, |
goto_functionst & | goto_functions | ||
) |
Definition at line 74 of file nondet_static.cpp.
References CPROVER_PREFIX, nondet_static(), and goto_functions_templatet< bodyT >::update().