cprover
|
Stack depth checks. More...
#include "stack_depth.h"
#include <util/arith_tools.h>
#include <goto-programs/goto_model.h>
#include <linking/static_lifetime_init.h>
Go to the source code of this file.
Functions | |
symbol_exprt | add_stack_depth_symbol (symbol_tablet &symbol_table) |
void | stack_depth (goto_programt &goto_program, const symbol_exprt &symbol, const int i_depth, const exprt &max_depth) |
void | stack_depth (goto_modelt &goto_model, const int depth) |
Stack depth checks.
Definition in file stack_depth.cpp.
symbol_exprt add_stack_depth_symbol | ( | symbol_tablet & | symbol_table | ) |
Definition at line 22 of file stack_depth.cpp.
References symbolt::base_name, from_integer(), symbol_tablet::insert(), symbolt::is_lvalue, symbolt::is_static_lifetime, symbolt::is_thread_local, symbolt::mode, symbolt::name, symbolt::pretty_name, symbolt::type, and symbolt::value.
Referenced by stack_depth().
void stack_depth | ( | goto_programt & | goto_program, |
const symbol_exprt & | symbol, | ||
const int | i_depth, | ||
const exprt & | max_depth | ||
) |
Definition at line 43 of file stack_depth.cpp.
References from_integer(), goto_program, goto_programt::insert_before(), goto_programt::insert_before_swap(), goto_programt::instructions, goto_programt::instructiont::make_assignment(), exprt::source_location(), to_string(), and exprt::type().
Referenced by goto_instrument_parse_optionst::instrument_goto_program(), and stack_depth().
void stack_depth | ( | goto_modelt & | goto_model, |
const int | depth | ||
) |
Definition at line 83 of file stack_depth.cpp.
References add_stack_depth_symbol(), DATA_INVARIANT, goto_functionst::entry_point(), Forall_goto_functions, from_integer(), goto_functionst::function_map, goto_modelt::goto_functions, INITIALIZE_FUNCTION, goto_programt::instructions, stack_depth(), goto_modelt::symbol_table, exprt::type(), and goto_functionst::update().