check_call_sequencet Class Reference

Collaboration diagram for check_call_sequencet:

Classes
struct	call_stack_entryt
struct	state_hash
struct	statet

Public Member Functions
	check_call_sequencet (const goto_modelt &_goto_model, const std::vector< irep_idt > &_sequence)
void	operator() ()

Protected Types
typedef std::unordered_set< statet, state_hash >	statest

Protected Attributes
const goto_functionst &	goto_functions
const std::vector< irep_idt > &	sequence
statest	states

Detailed Description

Definition at line 76 of file call_sequences.cpp.

Member Typedef Documentation

statest

typedef std::unordered_set<statet, state_hash> check_call_sequencet::statest

protected

Definition at line 138 of file call_sequences.cpp.

Constructor & Destructor Documentation

check_call_sequencet()

check_call_sequencet::check_call_sequencet ( const goto_modelt &  _goto_model, const std::vector< irep_idt > &  _sequence  )

inlineexplicit

Definition at line 79 of file call_sequences.cpp.

Member Function Documentation

operator()()

void check_call_sequencet::operator()

(

)

Definition at line 142 of file call_sequences.cpp.

Member Data Documentation

goto_functions

const goto_functionst& check_call_sequencet::goto_functions

protected

Definition at line 90 of file call_sequences.cpp.

sequence

const std::vector<irep_idt>& check_call_sequencet::sequence

protected

Definition at line 91 of file call_sequences.cpp.

states

statest check_call_sequencet::states

protected

Definition at line 139 of file call_sequences.cpp.

---

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

• /home/runner/work/cbmc/cbmc/src/goto-instrument/call_sequences.cpp