29 goto_functionst::function_mapt::iterator
37 const goto_programt::instructiont &instruction=*i_it;
39 if(instruction.is_assign())
56 i_it=init.insert_before(++i_it);
57 i_it->make_assignment();
59 i_it->source_location=instruction.source_location;
60 i_it->function=instruction.function;
62 else if(instruction.is_function_call())
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
const std::string & id2string(const irep_idt &d)
const irep_idt & get_identifier() const
Goto Programs with Functions.
bool get_bool(const irep_namet &name) const
const code_assignt & to_code_assign(const codet &code)
Nondeterministic initialization of certain global scope variables.
API to expression classes.
A side effect that returns a non-deterministically chosen value.
function_mapt function_map
bool has_prefix(const std::string &s, const std::string &prefix)
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
#define Forall_goto_program_instructions(it, program)
Expression to hold a symbol (variable)
void nondet_static(const namespacet &ns, goto_functionst &goto_functions, const irep_idt &fct_name)
const code_function_callt & to_code_function_call(const codet &code)