26 goto_functionst::function_mapt::iterator
48 .type.get_bool(ID_C_no_nondet_initialization))
68 i_it->function = original_instruction.
function;
irep_idt function
The function this instruction belongs to.
const std::string & id2string(const irep_idt &d)
bool is_function_call() const
const irep_idt & get_identifier() const
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
This class represents an instruction in the GOTO intermediate representation.
const code_assignt & to_code_assign(const codet &code)
#define INITIALIZE_FUNCTION
Nondeterministic initialization of certain global scope variables.
A side effect that returns a non-deterministically chosen value.
bool is_constant_or_has_constant_components(const typet &type, const namespacet &ns)
Identify if a given type is constant itself or contains constant components.
bool has_prefix(const std::string &s, const std::string &prefix)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
A generic container class for the GOTO intermediate representation of one function.
source_locationt source_location
The location of the instruction in the source file.
#define Forall_goto_program_instructions(it, program)
Expression to hold a symbol (variable)
goto_functionst goto_functions
GOTO functions.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
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)