cprover
check_call_sequencet Class Reference
Collaboration diagram for check_call_sequencet:
[legend]

Classes

struct  call_stack_entryt
 
struct  state_hash
 
struct  statet
 

Public Member Functions

 check_call_sequencet (const goto_functionst &_goto_functions, const std::vector< irep_idt > &_sequence)
 
void operator() ()
 

Protected Types

typedef std::unordered_set< statet, state_hashstatest
 

Protected Attributes

const goto_functionstgoto_functions
 
const std::vector< irep_idt > & sequence
 
statest states
 

Detailed Description

Definition at line 108 of file call_sequences.cpp.

Member Typedef Documentation

◆ statest

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

Definition at line 170 of file call_sequences.cpp.

Constructor & Destructor Documentation

◆ check_call_sequencet()

check_call_sequencet::check_call_sequencet ( const goto_functionst _goto_functions,
const std::vector< irep_idt > &  _sequence 
)
inlineexplicit

Definition at line 111 of file call_sequences.cpp.

Member Function Documentation

◆ operator()()

Member Data Documentation

◆ goto_functions

const goto_functionst& check_call_sequencet::goto_functions
protected

Definition at line 122 of file call_sequences.cpp.

Referenced by operator()().

◆ sequence

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

Definition at line 123 of file call_sequences.cpp.

Referenced by operator()().

◆ states

statest check_call_sequencet::states
protected

Definition at line 171 of file call_sequences.cpp.

Referenced by operator()().


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