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 }
make_integer_assignment
code_assignt make_integer_assignment(const symbol_table_baset &symbol_table, const irep_idt &symbol_name, T &&value)
Definition: add_malloc_may_fail_variable_initializations.cpp:15
symbol_table_baset::has_symbol
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
Definition: symbol_table_base.h:87
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
symbol_table_baset::lookup_ref
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:104
add_malloc_may_fail_variable_initializations.h
arith_tools.h
goto_model.h
Symbol Table + CFG.
goto_modelt
Definition: goto_model.h:26
configt::ansi_c
struct configt::ansi_ct ansi_c
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:29
goto_programt::make_assignment
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
Definition: goto_program.h:1082
goto_modelt::get_goto_functions
const goto_functionst & get_goto_functions() const override
Accessor to get a raw goto_functionst.
Definition: goto_model.h:72
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
INITIALIZE_FUNCTION
#define INITIALIZE_FUNCTION
Definition: static_lifetime_init.h:22
add_malloc_may_fail_variable_initializations
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 ...
Definition: add_malloc_may_fail_variable_initializations.cpp:24
config
configt config
Definition: config.cpp:25
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
config.h
configt::ansi_ct::malloc_failure_mode
malloc_failure_modet malloc_failure_mode
Definition: config.h:220
static_lifetime_init.h
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:293
configt::ansi_ct::malloc_may_fail
bool malloc_may_fail
Definition: config.h:211
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
irep.h