cprover
add_malloc_may_fail_variable_initializations.cpp
Go to the documentation of this file.
1 
5 
6 #include "goto_model.h"
7 
9 
10 #include <util/arith_tools.h>
11 #include <util/config.h>
12 #include <util/irep.h>
13 
14 template <typename T>
16  const symbol_table_baset &symbol_table,
17  const irep_idt &symbol_name,
18  T &&value)
19 {
20  const auto &symbol = symbol_table.lookup_ref(symbol_name).symbol_expr();
21  return code_assignt{symbol, from_integer(value, symbol.type())};
22 }
23 
25 {
26  const auto malloc_may_fail_id = irep_idt{CPROVER_PREFIX "malloc_may_fail"};
27  const auto malloc_failure_mode_id =
28  irep_idt{CPROVER_PREFIX "malloc_failure_mode"};
29  if(!goto_model.symbol_table.has_symbol(malloc_may_fail_id))
30  {
31  // if malloc_may_fail isn't in the symbol table (i.e. builtin library not
32  // loaded) then we don't generate initialisation code for it.
33  return;
34  }
35 
36  INVARIANT(
37  goto_model.symbol_table.has_symbol(malloc_failure_mode_id),
38  "if malloc_may_fail is in the symbol table then so should "
39  "malloc_failure_mode");
40 
41  auto const initialize_function_name = INITIALIZE_FUNCTION;
43  goto_model.get_goto_functions().function_map.count(
44  initialize_function_name) == 1);
45  auto &initialize_function =
46  goto_model.goto_functions.function_map.find(initialize_function_name)
47  ->second;
48  const auto initialize_function_end =
49  --initialize_function.body.instructions.end();
50 
51  initialize_function.body.insert_before(
52  initialize_function_end,
54  goto_model.symbol_table,
55  malloc_may_fail_id,
57 
58  initialize_function.body.insert_before(
59  initialize_function_end,
61  goto_model.symbol_table,
62  malloc_failure_mode_id,
64 }
code_assignt make_integer_assignment(const symbol_table_baset &symbol_table, const irep_idt &symbol_name, T &&value)
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 ...
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
A codet representing an assignment in the program.
Definition: std_code.h:295
struct configt::ansi_ct ansi_c
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
function_mapt function_map
const goto_functionst & get_goto_functions() const override
Accessor to get a raw goto_functionst.
Definition: goto_model.h:72
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
Definition: goto_program.h:995
The symbol table base class interface.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
configt config
Definition: config.cpp:24
#define CPROVER_PREFIX
Symbol Table + CFG.
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
#define INITIALIZE_FUNCTION
bool malloc_may_fail
Definition: config.h:212
malloc_failure_modet malloc_failure_mode
Definition: config.h:221