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.

◆ list_calls_and_arguments() [1/2]

void list_calls_and_arguments ( const goto_modelt & goto_model )

Definition at line 314 of file call_sequences.cpp.

◆ list_calls_and_arguments() [2/2]

static void list_calls_and_arguments	(	const namespacet &	ns,
		const goto_programt &	goto_program
	)

static

Definition at line 271 of file call_sequences.cpp.

◆ show_call_sequences() [1/2]

void show_call_sequences ( const goto_modelt & goto_model )

Definition at line 67 of file call_sequences.cpp.

◆ show_call_sequences() [2/2]

void show_call_sequences	(	const irep_idt &	caller,
		const goto_programt &	goto_program
	)

Definition at line 27 of file call_sequences.cpp.

Classes