cprover
|
#include "add_malloc_may_fail_variable_initializations.h"
#include "goto_model.h"
#include <util/arith_tools.h>
#include <util/config.h>
#include <util/irep.h>
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... | |
Definition in file add_malloc_may_fail_variable_initializations.cpp.
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.
code_assignt make_integer_assignment | ( | const symbol_table_baset & | symbol_table, |
const irep_idt & | symbol_name, | ||
T && | value | ||
) |
Definition at line 13 of file add_malloc_may_fail_variable_initializations.cpp.