#include <goto_symex_state.h>

Collaboration diagram for goto_symex_statet::framet:

Classes
struct	loop_infot

Public Attributes
irep_idt	function_identifier

goto_state_mapt	goto_state_map

symex_targett::sourcet	calling_location

goto_programt::const_targett	end_of_function

exprt	return_value = nil_exprt()

bool	hidden_function = false

symex_renaming_levelt::current_namest	old_level1

std::set< irep_idt >	local_objects

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

std::unordered_map< irep_idt, loop_infot >	loop_iterations

Detailed Description

Definition at line 174 of file goto_symex_state.h.

Member Data Documentation

◆ calling_location

symex_targett::sourcet goto_symex_statet::framet::calling_location

Definition at line 179 of file goto_symex_state.h.

◆ catch_map

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

Definition at line 190 of file goto_symex_state.h.

◆ end_of_function

goto_programt::const_targett goto_symex_statet::framet::end_of_function

Definition at line 181 of file goto_symex_state.h.

◆ function_identifier

irep_idt goto_symex_statet::framet::function_identifier

Definition at line 177 of file goto_symex_state.h.

◆ goto_state_map

goto_state_mapt goto_symex_statet::framet::goto_state_map

Definition at line 178 of file goto_symex_state.h.

◆ hidden_function

bool goto_symex_statet::framet::hidden_function = false

Definition at line 183 of file goto_symex_state.h.

◆ local_objects

std::set<irep_idt> goto_symex_statet::framet::local_objects

Definition at line 187 of file goto_symex_state.h.

◆ loop_iterations

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

Definition at line 198 of file goto_symex_state.h.

◆ old_level1

symex_renaming_levelt::current_namest goto_symex_statet::framet::old_level1

Definition at line 185 of file goto_symex_state.h.

◆ return_value

exprt goto_symex_statet::framet::return_value = nil_exprt()

Definition at line 182 of file goto_symex_state.h.

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

goto-symex/goto_symex_state.h

Classes

Public Attributes