CBMC
Loading...
Searching...
No Matches
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:
[フレーム]
[legend]

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:

AltStyle によって変換されたページ (->オリジナル) /