cprover
|
Printing function call sequences for Ofer. More...
#include "call_sequences.h"
#include <stack>
#include <iostream>
#include <util/simplify_expr.h>
#include <goto-programs/goto_model.h>
#include <langapi/language_util.h>
#include <linking/static_lifetime_init.h>
Go to the source code of this file.
Classes | |
class | check_call_sequencet |
struct | check_call_sequencet::call_stack_entryt |
struct | check_call_sequencet::statet |
struct | check_call_sequencet::state_hash |
Functions | |
void | show_call_sequences (const irep_idt &caller, const goto_programt &goto_program) |
void | show_call_sequences (const goto_modelt &goto_model) |
void | check_call_sequence (const goto_modelt &goto_model) |
static void | list_calls_and_arguments (const namespacet &ns, const goto_programt &goto_program) |
void | list_calls_and_arguments (const goto_modelt &goto_model) |
Printing function call sequences for Ofer.
Definition in file call_sequences.cpp.
void check_call_sequence | ( | const goto_modelt & | goto_model | ) |
Definition at line 252 of file call_sequences.cpp.
Referenced by goto_instrument_parse_optionst::doit().
|
static |
Definition at line 271 of file call_sequences.cpp.
References code_function_callt::arguments(), irept::find(), forall_goto_program_instructions, from_expr(), code_function_callt::function(), symbol_exprt::get_identifier(), goto_program, irept::id(), INITIALIZE_FUNCTION, simplify_expr(), size_type(), to_code_function_call(), and to_symbol_expr().
Referenced by goto_instrument_parse_optionst::doit(), and list_calls_and_arguments().
void list_calls_and_arguments | ( | const goto_modelt & | goto_model | ) |
Definition at line 316 of file call_sequences.cpp.
References forall_goto_functions, goto_modelt::goto_functions, list_calls_and_arguments(), and goto_modelt::symbol_table.
void show_call_sequences | ( | const irep_idt & | caller, |
const goto_programt & | goto_program | ||
) |
Definition at line 27 of file call_sequences.cpp.
References code_function_callt::function(), symbol_exprt::get_identifier(), goto_programt::get_successors(), goto_program, irept::id(), goto_programt::instructions, stack, to_code_function_call(), and to_symbol_expr().
Referenced by goto_instrument_parse_optionst::doit(), and show_call_sequences().
void show_call_sequences | ( | const goto_modelt & | goto_model | ) |
Definition at line 67 of file call_sequences.cpp.
References forall_goto_functions, goto_modelt::goto_functions, and show_call_sequences().