CBMC
Public Types | Public Member Functions | Public Attributes | List of all members
goto_trace_stept Class Reference

Step of the trace of a GOTO program. More...

#include <goto_trace.h>

+ Collaboration diagram for goto_trace_stept:

Public Types

enum class  typet {
  NONE , ASSIGNMENT , ASSUME , ASSERT ,
  GOTO , LOCATION , INPUT , OUTPUT ,
  DECL , DEAD , FUNCTION_CALL , FUNCTION_RETURN ,
  CONSTRAINT , SHARED_READ , SHARED_WRITE , SPAWN ,
  MEMORY_BARRIER , ATOMIC_BEGIN , ATOMIC_END
}
 
enum class  assignment_typet { STATE , ACTUAL_PARAMETER }
 
typedef std::list< exprt > io_argst
 

Public Member Functions

bool is_assignment () const
 
bool is_assume () const
 
bool is_assert () const
 
bool is_goto () const
 
bool is_constraint () const
 
bool is_function_call () const
 
bool is_function_return () const
 
bool is_location () const
 
bool is_output () const
 
bool is_input () const
 
bool is_decl () const
 
bool is_dead () const
 
bool is_shared_read () const
 
bool is_shared_write () const
 
bool is_spawn () const
 
bool is_memory_barrier () const
 
bool is_atomic_begin () const
 
bool is_atomic_end () const
 
std::optional< symbol_exprt > get_lhs_object () const
 
void output (const class namespacet &ns, std::ostream &out) const
 Outputs the trace step in ASCII to a given stream. More...
 
 goto_trace_stept ()
 
void merge_ireps (merge_irept &dest)
 Use dest to establish sharing among ireps. More...
 

Public Attributes

std::size_t step_nr
 Number of the step in the trace. More...
 
typet type
 
bool hidden
 
bool internal
 
assignment_typet assignment_type
 
irep_idt function_id
 
goto_programt::const_targett pc
 
unsigned thread_nr
 
bool cond_value
 
exprt cond_expr
 
exprt original_condition
 
irep_idt property_id
 
std::string comment
 
exprt full_lhs
 
exprt full_lhs_value
 
irep_idt format_string
 
irep_idt io_id
 
io_argst io_args
 
bool formatted
 
irep_idt called_function
 
std::vector< exprt > function_arguments
 

Detailed Description

Step of the trace of a GOTO program.

A step is either:

  • an assignment
  • an assume statement
  • an assertion
  • a goto instruction
  • a constraint (unused)
  • a function call
  • a function return
  • a location (unused)
  • an output
  • an input
  • a declaration
  • a dead statement
  • a shared read (unused)
  • a shared write (unused)
  • a spawn statement
  • a memory barrier
  • an atomic begin (unused)
  • an atomic end (unused)

Definition at line 49 of file goto_trace.h.

Member Typedef Documentation

◆ io_argst

typedef std::list<exprt> goto_trace_stept::io_argst

Definition at line 137 of file goto_trace.h.

Member Enumeration Documentation

◆ assignment_typet

enum goto_trace_stept::assignment_typet
strong
Enumerator
STATE 
ACTUAL_PARAMETER 

Definition at line 106 of file goto_trace.h.

◆ typet

enum goto_trace_stept::typet
strong
Enumerator
NONE 
ASSIGNMENT 
ASSUME 
ASSERT 
GOTO 
LOCATION 
INPUT 
OUTPUT 
DECL 
DEAD 
FUNCTION_CALL 
FUNCTION_RETURN 
CONSTRAINT 
SHARED_READ 
SHARED_WRITE 
SPAWN 
MEMORY_BARRIER 
ATOMIC_BEGIN 
ATOMIC_END 

Definition at line 74 of file goto_trace.h.

Constructor & Destructor Documentation

◆ goto_trace_stept()

goto_trace_stept::goto_trace_stept ( )
inline

Definition at line 152 of file goto_trace.h.

Member Function Documentation

◆ get_lhs_object()

std::optional< symbol_exprt > goto_trace_stept::get_lhs_object ( ) const

Definition at line 53 of file goto_trace.cpp.

◆ is_assert()

bool goto_trace_stept::is_assert ( ) const
inline

Definition at line 57 of file goto_trace.h.

◆ is_assignment()

bool goto_trace_stept::is_assignment ( ) const
inline

Definition at line 55 of file goto_trace.h.

◆ is_assume()

bool goto_trace_stept::is_assume ( ) const
inline

Definition at line 56 of file goto_trace.h.

◆ is_atomic_begin()

bool goto_trace_stept::is_atomic_begin ( ) const
inline

Definition at line 71 of file goto_trace.h.

◆ is_atomic_end()

bool goto_trace_stept::is_atomic_end ( ) const
inline

Definition at line 72 of file goto_trace.h.

◆ is_constraint()

bool goto_trace_stept::is_constraint ( ) const
inline

Definition at line 59 of file goto_trace.h.

◆ is_dead()

bool goto_trace_stept::is_dead ( ) const
inline

Definition at line 66 of file goto_trace.h.

◆ is_decl()

bool goto_trace_stept::is_decl ( ) const
inline

Definition at line 65 of file goto_trace.h.

◆ is_function_call()

bool goto_trace_stept::is_function_call ( ) const
inline

Definition at line 60 of file goto_trace.h.

◆ is_function_return()

bool goto_trace_stept::is_function_return ( ) const
inline

Definition at line 61 of file goto_trace.h.

◆ is_goto()

bool goto_trace_stept::is_goto ( ) const
inline

Definition at line 58 of file goto_trace.h.

◆ is_input()

bool goto_trace_stept::is_input ( ) const
inline

Definition at line 64 of file goto_trace.h.

◆ is_location()

bool goto_trace_stept::is_location ( ) const
inline

Definition at line 62 of file goto_trace.h.

◆ is_memory_barrier()

bool goto_trace_stept::is_memory_barrier ( ) const
inline

Definition at line 70 of file goto_trace.h.

◆ is_output()

bool goto_trace_stept::is_output ( ) const
inline

Definition at line 63 of file goto_trace.h.

◆ is_shared_read()

bool goto_trace_stept::is_shared_read ( ) const
inline

Definition at line 67 of file goto_trace.h.

◆ is_shared_write()

bool goto_trace_stept::is_shared_write ( ) const
inline

Definition at line 68 of file goto_trace.h.

◆ is_spawn()

bool goto_trace_stept::is_spawn ( ) const
inline

Definition at line 69 of file goto_trace.h.

◆ merge_ireps()

void goto_trace_stept::merge_ireps ( merge_irept &  dest)

Use dest to establish sharing among ireps.

Parameters
[out]destirep storage container.

Definition at line 141 of file goto_trace.cpp.

◆ output()

void goto_trace_stept::output ( const class namespacet &  ns,
std::ostream &  out 
) const

Outputs the trace step in ASCII to a given stream.

Definition at line 66 of file goto_trace.cpp.

Member Data Documentation

◆ assignment_type

assignment_typet goto_trace_stept::assignment_type

Definition at line 107 of file goto_trace.h.

◆ called_function

irep_idt goto_trace_stept::called_function

Definition at line 142 of file goto_trace.h.

◆ comment

std::string goto_trace_stept::comment

Definition at line 124 of file goto_trace.h.

◆ cond_expr

exprt goto_trace_stept::cond_expr

Definition at line 119 of file goto_trace.h.

◆ cond_value

bool goto_trace_stept::cond_value

Definition at line 118 of file goto_trace.h.

◆ format_string

irep_idt goto_trace_stept::format_string

Definition at line 136 of file goto_trace.h.

◆ formatted

bool goto_trace_stept::formatted

Definition at line 139 of file goto_trace.h.

◆ full_lhs

exprt goto_trace_stept::full_lhs

Definition at line 127 of file goto_trace.h.

◆ full_lhs_value

exprt goto_trace_stept::full_lhs_value

Definition at line 133 of file goto_trace.h.

◆ function_arguments

std::vector<exprt> goto_trace_stept::function_arguments

Definition at line 145 of file goto_trace.h.

◆ function_id

irep_idt goto_trace_stept::function_id

Definition at line 111 of file goto_trace.h.

◆ hidden

bool goto_trace_stept::hidden

Definition at line 100 of file goto_trace.h.

◆ internal

bool goto_trace_stept::internal

Definition at line 103 of file goto_trace.h.

◆ io_args

io_argst goto_trace_stept::io_args

Definition at line 138 of file goto_trace.h.

◆ io_id

irep_idt goto_trace_stept::io_id

Definition at line 136 of file goto_trace.h.

◆ original_condition

exprt goto_trace_stept::original_condition

Definition at line 120 of file goto_trace.h.

◆ pc

goto_programt::const_targett goto_trace_stept::pc

Definition at line 112 of file goto_trace.h.

◆ property_id

irep_idt goto_trace_stept::property_id

Definition at line 123 of file goto_trace.h.

◆ step_nr

std::size_t goto_trace_stept::step_nr

Number of the step in the trace.

Definition at line 53 of file goto_trace.h.

◆ thread_nr

unsigned goto_trace_stept::thread_nr

Definition at line 115 of file goto_trace.h.

◆ type

typet goto_trace_stept::type

Definition at line 97 of file goto_trace.h.

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