nondet_static.cpp File Reference

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>

Include dependency graph for nondet_static.cpp:

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)

Detailed Description

Nondeterministic initialization of certain global scope variables.

Definition in file nondet_static.cpp.

Function Documentation

nondet_static() [1/2]

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().

nondet_static() [2/2]

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().