goto_symex_statet::framet Class Reference

Stack frame tracking class. More...

#include <goto_symex_state.h>

Public Member Functions
void	grow_stack_frame (const expr2tc &expr)
	Add the storage expr occupies, in bits, to this frame's running total.
void	decrease_stack_frame_size (const expr2tc &expr)
	Decrease the stack frame size when the variables go out of scope.
	framet (unsigned int thread_id, const namespacet *ns=nullptr)

Public Attributes
irep_idt	function_identifier
	Name of function called to make this stack frame.
merge_state_mapt	merge_state_map
	Map of symbolic snapshots to merge in the future.
renaming::level1t	level1
	Renaming context for L1 names.
symex_targett::sourcet	calling_location
	Record of source of function call.
goto_programt::const_targett	end_of_function
	End of function instruction location.
expr2tc	return_value
	Expression to assign return values to.
std::list< std::pair< goto_programt::const_targett, expr2tc > >	cur_function_ptr_targets
	List of function pointer targets.
goto_programt::const_targett	function_ptr_call_loc
	Instruction where function pointer calls should seem to originate from.
goto_programt::const_targett	function_ptr_combine_target
	Function pointer call merge point.
expr2tc	orig_func_ptr_call
	Original function pointer call code.
variable_name_sett	declaration_history
	Set of variables names that have been declared.
variable_name_sett	local_variables
	Set of local variable l1 names.
std::vector< expr2tc >	alloca_objects
	Pointers returned by alloca in this frame; their objects die when the frame returns, not at the end of the enclosing block (alloca(3)).
unsigned int	va_index
	Record the first va_args index used in this function call, if any, otherwise UINT_MAX.
unsigned int	va_cursor
	Cursor into this activation's va_args, advanced by each va_arg use.
guard2tc	entry_guard
	Record the entry guard of the function.
bool	hidden
	Record if the function body is hidden.
BigInt	stack_frame_total
	The stack size of the frame.

Detailed Description

Stack frame tracking class.

Records all information relevant to a particular stack frame created by the invocation of a function call. Has a renaming context and level 1 "activation record" ID number to stop recursive calls aliasing. Also contains function-return data, and the set of states that need to be merged as the result of jumps in the past. Primarily a data container.

Constructor & Destructor Documentation

framet()

goto_symex_statet::framet::framet ( unsigned int thread_id, const namespacet * ns = nullptr )

inline

Member Function Documentation

decrease_stack_frame_size()

void goto_symex_statet::framet::decrease_stack_frame_size

(

const expr2tc &

expr

)

Decrease the stack frame size when the variables go out of scope.

Parameters

expr	Expression to considered in the stack frame.

grow_stack_frame()

void goto_symex_statet::framet::grow_stack_frame

(

const expr2tc &

expr

)

Add the storage expr occupies, in bits, to this frame's running total.

Parameters

expr	Expr whose type gives the storage to account for.

Member Data Documentation

alloca_objects

std::vector<expr2tc> goto_symex_statet::framet::alloca_objects

Pointers returned by alloca in this frame; their objects die when the frame returns, not at the end of the enclosing block (alloca(3)).

calling_location

symex_targett::sourcet goto_symex_statet::framet::calling_location

Record of source of function call.

Used when returning from the function to the caller.

cur_function_ptr_targets

std::list<std::pair<goto_programt::const_targett, expr2tc> > goto_symex_statet::framet::cur_function_ptr_targets

List of function pointer targets.

During the invocation of a function pointer call, this contains a list of targets that the function pointer can point at, and that need to have calls set up to and executed. This member contains an iterator to the first goto instruction in the target and the target symbol name.

declaration_history

variable_name_sett goto_symex_statet::framet::declaration_history

Set of variables names that have been declared.

Used to detect when we are in some kind of block that is entered then exited repeatedly - whenever that happens, a new l1 name is required unless symex_decl can reuse the dead one. This caches the already seen names in a function for making that decision.

end_of_function

goto_programt::const_targett goto_symex_statet::framet::end_of_function

End of function instruction location.

Jumped to after an in-body return instruction.

entry_guard

guard2tc goto_symex_statet::framet::entry_guard

Record the entry guard of the function.

function_identifier

irep_idt goto_symex_statet::framet::function_identifier

Name of function called to make this stack frame.

function_ptr_call_loc

goto_programt::const_targett goto_symex_statet::framet::function_ptr_call_loc

Instruction where function pointer calls should seem to originate from.

function_ptr_combine_target

goto_programt::const_targett goto_symex_statet::framet::function_ptr_combine_target

Function pointer call merge point.

Instruction where the resulting states from particular funtion calls originating from a function pointer dereference should be merged into main state.

hidden

bool goto_symex_statet::framet::hidden

Record if the function body is hidden.

level1

renaming::level1t goto_symex_statet::framet::level1

Renaming context for L1 names.

local_variables

variable_name_sett goto_symex_statet::framet::local_variables

Set of local variable l1 names.

merge_state_map

merge_state_mapt goto_symex_statet::framet::merge_state_map

Map of symbolic snapshots to merge in the future.

Each entry records the merge-relevant state for a path that reaches a particular instruction and must be joined by phi_function.

orig_func_ptr_call

expr2tc goto_symex_statet::framet::orig_func_ptr_call

Original function pointer call code.

Contains arguments to setup resulting function invocations with.

return_value

expr2tc goto_symex_statet::framet::return_value

Expression to assign return values to.

The lvalue that the calller assigns the result of this function call to at a higher level.

stack_frame_total

BigInt goto_symex_statet::framet::stack_frame_total

The stack size of the frame.

va_cursor

unsigned int goto_symex_statet::framet::va_cursor

Cursor into this activation's va_args, advanced by each va_arg use.

Starts equal to va_index. va_cursor == va_index means no argument has been consumed yet; symex_printf's va_list recovery relies on this (after any consumption a va_start rewind is indistinguishable from further consumption, so recovery must decline).

va_index

unsigned int goto_symex_statet::framet::va_index

Record the first va_args index used in this function call, if any, otherwise UINT_MAX.

---

The documentation for this class was generated from the following files:

• src/goto-symex/state/goto_symex_state.h
• src/goto-symex/engine/symex_stack.cpp