Stack frames – these are used for function calls and for exceptions. More...

#include <frame.h>

Collaboration diagram for framet:

Classes
class	active_loop_infot

struct	loop_infot

Public Types
using	goto_state_listt = std::list< std::pair< symex_targett::sourcet, goto_statet > >

Public Member Functions
	framet (symex_targett::sourcet _calling_location, const guardt &state_guard)

Public Attributes
irep_idt	function_identifier

std::map< goto_programt::const_targett, goto_state_listt >	goto_state_map

symex_targett::sourcet	calling_location

std::vector< irep_idt >	parameter_names

guardt	guard_at_function_start

goto_programt::const_targett	end_of_function

exprt	call_lhs = nil_exprt()

optionalt< symbol_exprt >	return_value_symbol

bool	hidden_function = false

symex_level1t	old_level1

std::set< irep_idt >	local_objects

std::map< irep_idt, goto_programt::targett >	catch_map

std::shared_ptr< lexical_loopst >	loops_info

std::vector< active_loop_infot >	active_loops

std::unordered_map< irep_idt, loop_infot >	loop_iterations

Detailed Description

Stack frames – these are used for function calls and for exceptions.

Definition at line 21 of file frame.h.

Member Typedef Documentation

◆ goto_state_listt

using framet::goto_state_listt = std::list<std::pair<symex_targett::sourcet, goto_statet> >

Definition at line 25 of file frame.h.

Constructor & Destructor Documentation

◆ framet()

framet::framet	(	symex_targett::sourcet	_calling_location,
		const guardt &	state_guard
	)

inline

Definition at line 75 of file frame.h.

Member Data Documentation

◆ active_loops

std::vector<active_loop_infot> framet::active_loops

Definition at line 71 of file frame.h.

◆ call_lhs

exprt framet::call_lhs = nil_exprt()

Definition at line 34 of file frame.h.

◆ calling_location

symex_targett::sourcet framet::calling_location

Definition at line 30 of file frame.h.

◆ catch_map

std::map<irep_idt, goto_programt::targett> framet::catch_map

Definition at line 43 of file frame.h.

◆ end_of_function

goto_programt::const_targett framet::end_of_function

Definition at line 33 of file frame.h.

◆ function_identifier

irep_idt framet::function_identifier

Definition at line 28 of file frame.h.

◆ goto_state_map

std::map<goto_programt::const_targett, goto_state_listt> framet::goto_state_map

Definition at line 29 of file frame.h.

◆ guard_at_function_start

guardt framet::guard_at_function_start

Definition at line 32 of file frame.h.

◆ hidden_function

bool framet::hidden_function = false

Definition at line 36 of file frame.h.

◆ local_objects

std::set<irep_idt> framet::local_objects

Definition at line 40 of file frame.h.

◆ loop_iterations

std::unordered_map<irep_idt, loop_infot> framet::loop_iterations

Definition at line 73 of file frame.h.

◆ loops_info

std::shared_ptr<lexical_loopst> framet::loops_info

Definition at line 70 of file frame.h.

◆ old_level1

symex_level1t framet::old_level1

Definition at line 38 of file frame.h.

◆ parameter_names

std::vector<irep_idt> framet::parameter_names

Definition at line 31 of file frame.h.

◆ return_value_symbol

optionalt<symbol_exprt> framet::return_value_symbol

Definition at line 35 of file frame.h.

The documentation for this struct was generated from the following file:

/home/runner/work/cbmc-documentation/cbmc-documentation/src/goto-symex/frame.h

Classes

Public Types

Public Member Functions

Public Attributes