Go to the documentation of this file.
25 const auto malloc_failure_mode_id =
36 "if malloc_may_fail is in the symbol table then so should "
37 "malloc_failure_mode");
42 initialize_function_name) == 1);
43 auto &initialize_function =
46 const auto initialize_function_end =
47 --initialize_function.body.instructions.end();
49 initialize_function.body.insert_before(
50 initialize_function_end,
56 initialize_function.body.insert_before(
57 initialize_function_end,
60 malloc_failure_mode_id,
code_assignt make_integer_assignment(const symbol_table_baset &symbol_table, const irep_idt &symbol_name, T &&value)
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
struct configt::ansi_ct ansi_c
function_mapt function_map
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
const goto_functionst & get_goto_functions() const override
Accessor to get a raw goto_functionst.
#define PRECONDITION(CONDITION)
The symbol table base class interface.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
void add_malloc_may_fail_variable_initializations(goto_modelt &goto_model)
Some variables have different initial values based on what flags are being passed to cbmc; since the ...
goto_functionst goto_functions
GOTO functions.
malloc_failure_modet malloc_failure_mode
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
A codet representing an assignment in the program.
symbol_tablet symbol_table
Symbol table.