cprover
|
Nondeterministic initialization of certain global scope variables. More...
#include "nondet_static.h"
#include <goto-programs/goto_model.h>
#include <linking/static_lifetime_init.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) |
void | nondet_static (goto_modelt &goto_model) |
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 21 of file nondet_static.cpp.
References goto_programt::instructiont::code, CPROVER_PREFIX, Forall_goto_program_instructions, goto_programt::instructiont::function, code_function_callt::function(), goto_functionst::function_map, symbol_exprt::get_identifier(), has_prefix(), id2string(), goto_programt::instructiont::is_assign(), is_constant_or_has_constant_components(), goto_programt::instructiont::is_function_call(), code_assignt::lhs(), namespacet::lookup(), goto_programt::instructiont::source_location, to_code_assign(), to_code_function_call(), to_symbol_expr(), and exprt::type().
Referenced by goto_instrument_parse_optionst::instrument_goto_program(), nondet_static(), jbmc_parse_optionst::process_goto_functions(), and cbmc_parse_optionst::process_goto_program().
void nondet_static | ( | const namespacet & | ns, |
goto_functionst & | goto_functions | ||
) |
Definition at line 70 of file nondet_static.cpp.
References INITIALIZE_FUNCTION, nondet_static(), and goto_functionst::update().
void nondet_static | ( | goto_modelt & | goto_model | ) |
Definition at line 80 of file nondet_static.cpp.
References goto_modelt::goto_functions, nondet_static(), and goto_modelt::symbol_table.