cprover
add_malloc_may_fail_variable_initializations.cpp File Reference
+ Include dependency graph for add_malloc_may_fail_variable_initializations.cpp:

Go to the source code of this file.

Functions

template<typename T >
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 _start function might've been generated by goto-cc before getting passed over here we need to add the initialisation of these variables here as a post-processing step. More...
 

Detailed Description

Author
Diffblue Ltd.

Definition in file add_malloc_may_fail_variable_initializations.cpp.

Function Documentation

◆ 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 _start function might've been generated by goto-cc before getting passed over here we need to add the initialisation of these variables here as a post-processing step.

Definition at line 22 of file add_malloc_may_fail_variable_initializations.cpp.

◆ make_integer_assignment()

template<typename T >
code_assignt make_integer_assignment ( const symbol_table_baset symbol_table,
const irep_idt symbol_name,
T &&  value 
)