cprover
add_malloc_may_fail_variable_initializations.cpp
Go to the documentation of this file.
1 
5 
6 #include "goto_model.h"
7 
8 #include <util/arith_tools.h>
9 #include <util/config.h>
10 #include <util/irep.h>
11 
12 template <typename T>
14  const symbol_table_baset &symbol_table,
15  const irep_idt &symbol_name,
16  T &&value)
17 {
18  const auto &symbol = symbol_table.lookup_ref(symbol_name).symbol_expr();
19  return code_assignt{symbol, from_integer(value, symbol.type())};
20 }
21 
23 {
24  const auto malloc_may_fail_id = irep_idt{CPROVER_PREFIX "malloc_may_fail"};
25  const auto malloc_failure_mode_id =
26  irep_idt{CPROVER_PREFIX "malloc_failure_mode"};
27  if(!goto_model.symbol_table.has_symbol(malloc_may_fail_id))
28  {
29  // if malloc_may_fail isn't in the symbol table (i.e. builtin library not
30  // loaded) then we don't generate initialisation code for it.
31  return;
32  }
33 
34  INVARIANT(
35  goto_model.symbol_table.has_symbol(malloc_failure_mode_id),
36  "if malloc_may_fail is in the symbol table then so should "
37  "malloc_failure_mode");
38 
39  auto const initialize_function_name = CPROVER_PREFIX "initialize";
41  goto_model.get_goto_functions().function_map.count(
42  initialize_function_name) == 1);
43  auto &initialize_function =
44  goto_model.goto_functions.function_map.find(initialize_function_name)
45  ->second;
46  const auto initialize_function_end =
47  --initialize_function.body.instructions.end();
48 
49  initialize_function.body.insert_before(
50  initialize_function_end,
52  goto_model.symbol_table,
53  malloc_may_fail_id,
55 
56  initialize_function.body.insert_before(
57  initialize_function_end,
59  goto_model.symbol_table,
60  malloc_failure_mode_id,
62 }
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:13
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:27
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:1024
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:464
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:122
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:22
config
configt config
Definition: config.cpp:24
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:141
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
configt::ansi_ct::malloc_may_fail
bool malloc_may_fail
Definition: config.h:132
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
irep.h