cprover
|
Printing function call sequences for Ofer. More...
#include "call_sequences.h"
#include <stack>
#include <iostream>
#include <unordered_set>
#include <util/std_expr.h>
#include <util/simplify_expr.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 &function, const goto_programt &goto_program, const goto_programt::const_targett start) |
void | show_call_sequences (const irep_idt &function, const goto_programt &goto_program) |
void | show_call_sequences (const goto_functionst &goto_functions) |
void | check_call_sequence (const goto_functionst &goto_functions) |
static void | list_calls_and_arguments (const namespacet &ns, const irep_idt &function, const goto_programt &goto_program) |
void | list_calls_and_arguments (const namespacet &ns, const goto_functionst &goto_functions) |
Printing function call sequences for Ofer.
Definition in file call_sequences.cpp.
void check_call_sequence | ( | const goto_functionst & | goto_functions | ) |
Definition at line 284 of file call_sequences.cpp.
References check_call_sequencet::check_call_sequencet(), and check_call_sequencet::sequence.
Referenced by goto_instrument_parse_optionst::doit().
|
static |
Definition at line 303 of file call_sequences.cpp.
References code_function_callt::arguments(), check_call_sequencet::call_stack_entryt::f, irept::find(), forall_goto_program_instructions, from_expr(), code_function_callt::function(), symbol_exprt::get_identifier(), irept::id(), 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 namespacet & | ns, |
const goto_functionst & | goto_functions | ||
) |
Definition at line 349 of file call_sequences.cpp.
References forall_goto_functions, and list_calls_and_arguments().
void show_call_sequences | ( | const irep_idt & | function, |
const goto_programt & | goto_program, | ||
const goto_programt::const_targett | start | ||
) |
Definition at line 23 of file call_sequences.cpp.
References code_function_callt::function(), symbol_exprt::get_identifier(), goto_program_templatet< codeT, guardT >::get_successors(), irept::id(), goto_program_templatet< codeT, guardT >::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 irep_idt & | function, |
const goto_programt & | goto_program | ||
) |
Definition at line 64 of file call_sequences.cpp.
References forall_goto_program_instructions, code_function_callt::function(), irept::id(), goto_program_templatet< codeT, guardT >::instructions, show_call_sequences(), to_code_function_call(), and to_symbol_expr().
void show_call_sequences | ( | const goto_functionst & | goto_functions | ) |
Definition at line 100 of file call_sequences.cpp.
References forall_goto_functions, and show_call_sequences().