cprover
|
Stack depth checks. More...
#include "stack_depth.h"
#include <util/symbol_table.h>
#include <util/std_expr.h>
#include <util/std_types.h>
#include <util/arith_tools.h>
#include <util/cprover_prefix.h>
#include <goto-programs/goto_functions.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 (symbol_tablet &symbol_table, goto_functionst &goto_functions, 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 24 of file stack_depth.cpp.
References symbolt::base_name, from_integer(), symbolt::is_lvalue, symbolt::is_static_lifetime, symbolt::is_thread_local, symbolt::mode, symbol_tablet::move(), 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 45 of file stack_depth.cpp.
References from_integer(), goto_program_templatet< codeT, guardT >::insert_before(), goto_program_templatet< codeT, guardT >::insert_before_swap(), goto_program_templatet< codeT, guardT >::instructions, exprt::source_location(), and exprt::type().
Referenced by goto_instrument_parse_optionst::instrument_goto_program(), and stack_depth().
void stack_depth | ( | symbol_tablet & | symbol_table, |
goto_functionst & | goto_functions, | ||
const int | depth | ||
) |
Definition at line 85 of file stack_depth.cpp.
References add_stack_depth_symbol(), CPROVER_PREFIX, goto_functions_templatet< goto_programt >::entry_point(), Forall_goto_functions, from_integer(), goto_functions_templatet< bodyT >::function_map, stack_depth(), exprt::type(), and goto_functions_templatet< bodyT >::update().