cprover
call_sequences.cpp File Reference

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>
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 &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)
 

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_modelt goto_model)

Definition at line 252 of file call_sequences.cpp.

Referenced by goto_instrument_parse_optionst::doit().

◆ list_calls_and_arguments() [1/2]

◆ list_calls_and_arguments() [2/2]

void list_calls_and_arguments ( const goto_modelt goto_model)

◆ show_call_sequences() [1/2]

◆ show_call_sequences() [2/2]

void show_call_sequences ( const goto_modelt goto_model)