CBMC
Classes | Public Types | Public Member Functions | Public Attributes | List of all members
framet Struct Reference

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

#include <solver_types.h>

+ Collaboration diagram for framet:

Classes

class  active_loop_infot
 
struct  implicationt
 
struct  loop_infot
 

Public Types

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

Public Member Functions

 framet (symbol_exprt __symbol, source_locationt __source_location, frame_reft __ref)
 
void add_auxiliary (exprt)
 
void add_invariant (exprt)
 
void add_obligation (exprt)
 
void reset ()
 
 framet (symex_targett::sourcet _calling_location, const guardt &state_guard)
 

Public Attributes

symbol_exprt symbol
 
std::vector< exprt > invariants
 
std::unordered_set< exprt, irep_hash > invariants_set
 
std::vector< exprt > obligations
 
std::unordered_set< exprt, irep_hash > obligations_set
 
std::vector< exprt > auxiliaries
 
std::unordered_set< exprt, irep_hash > auxiliaries_set
 
std::vector< implicationt > implications
 
source_locationt source_location = source_locationt::nil()
 
frame_reft ref
 
irep_idt function_identifier
 
std::map< goto_programt::const_targett, goto_state_listt, goto_programt::target_less_than > 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()
 
std::optional< 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 40 of file solver_types.h.

Member Typedef Documentation

◆ goto_state_listt

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

Definition at line 24 of file frame.h.

Constructor & Destructor Documentation

◆ framet() [1/2]

framet::framet ( symbol_exprt  __symbol,
source_locationt  __source_location,
frame_reft  __ref 
)
inline

Definition at line 43 of file solver_types.h.

◆ framet() [2/2]

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

Definition at line 79 of file frame.h.

Member Function Documentation

◆ add_auxiliary()

void framet::add_auxiliary ( exprt  invariant)

Definition at line 21 of file solver_types.cpp.

◆ add_invariant()

void framet::add_invariant ( exprt  invariant)

Definition at line 35 of file solver_types.cpp.

◆ add_obligation()

void framet::add_obligation ( exprt  obligation)

Definition at line 49 of file solver_types.cpp.

◆ reset()

void framet::reset ( )
inline

Definition at line 92 of file solver_types.h.

Member Data Documentation

◆ active_loops

std::vector<active_loop_infot> framet::active_loops

Definition at line 75 of file frame.h.

◆ auxiliaries

std::vector<exprt> framet::auxiliaries

Definition at line 64 of file solver_types.h.

◆ auxiliaries_set

std::unordered_set<exprt, irep_hash> framet::auxiliaries_set

Definition at line 65 of file solver_types.h.

◆ call_lhs

exprt framet::call_lhs = nil_exprt()

Definition at line 38 of file frame.h.

◆ calling_location

symex_targett::sourcet framet::calling_location

Definition at line 34 of file frame.h.

◆ catch_map

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

Definition at line 47 of file frame.h.

◆ end_of_function

goto_programt::const_targett framet::end_of_function

Definition at line 37 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, goto_programt::target_less_than> framet::goto_state_map

Definition at line 33 of file frame.h.

◆ guard_at_function_start

guardt framet::guard_at_function_start

Definition at line 36 of file frame.h.

◆ hidden_function

bool framet::hidden_function = false

Definition at line 40 of file frame.h.

◆ implications

std::vector<implicationt> framet::implications

Definition at line 83 of file solver_types.h.

◆ invariants

std::vector<exprt> framet::invariants

Definition at line 56 of file solver_types.h.

◆ invariants_set

std::unordered_set<exprt, irep_hash> framet::invariants_set

Definition at line 57 of file solver_types.h.

◆ local_objects

std::set<irep_idt> framet::local_objects

Definition at line 44 of file frame.h.

◆ loop_iterations

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

Definition at line 77 of file frame.h.

◆ loops_info

std::shared_ptr<lexical_loopst> framet::loops_info

Definition at line 74 of file frame.h.

◆ obligations

std::vector<exprt> framet::obligations

Definition at line 60 of file solver_types.h.

◆ obligations_set

std::unordered_set<exprt, irep_hash> framet::obligations_set

Definition at line 61 of file solver_types.h.

◆ old_level1

symex_level1t framet::old_level1

Definition at line 42 of file frame.h.

◆ parameter_names

std::vector<irep_idt> framet::parameter_names

Definition at line 35 of file frame.h.

◆ ref

frame_reft framet::ref

Definition at line 102 of file solver_types.h.

◆ return_value_symbol

std::optional<symbol_exprt> framet::return_value_symbol

Definition at line 39 of file frame.h.

◆ source_location

source_locationt framet::source_location = source_locationt::nil()

Definition at line 86 of file solver_types.h.

◆ symbol

symbol_exprt framet::symbol

Definition at line 53 of file solver_types.h.

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