cprover
call_sequences.cpp File Reference

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>
Include dependency graph for call_sequences.cpp:

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)
 

Detailed Description

Printing function call sequences for Ofer.

Definition in file call_sequences.cpp.

Function Documentation

§ check_call_sequence()

void check_call_sequence ( const goto_functionst goto_functions)

§ list_calls_and_arguments() [1/2]

§ list_calls_and_arguments() [2/2]

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().

§ show_call_sequences() [1/3]

§ show_call_sequences() [2/3]

§ show_call_sequences() [3/3]

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().