CBMC
Public Member Functions | Public Attributes | List of all members
symex_targett::sourcet Struct Reference

Identifies source in the context of symbolic execution. More...

#include <symex_target.h>

+ Collaboration diagram for symex_targett::sourcet:

Public Member Functions

 sourcet (const irep_idt &_function_id, goto_programt::const_targett _pc)
 
 sourcet (const irep_idt &_function_id, const goto_programt &_goto_program)
 
 sourcet (sourcet &&other) noexcept
 
 sourcet (const sourcet &other)=default
 
sourcet & operator= (const sourcet &other)=default
 
sourcet & operator= (sourcet &&other)=default
 

Public Attributes

unsigned thread_nr
 
irep_idt function_id
 
goto_programt::const_targett pc
 

Detailed Description

Identifies source in the context of symbolic execution.

Thread number thread_nr is zero by default and the program counter pc points to the first instruction of the input GOTO program.

Definition at line 36 of file symex_target.h.

Constructor & Destructor Documentation

◆ sourcet() [1/4]

symex_targett::sourcet::sourcet ( const irep_idt &  _function_id,
goto_programt::const_targett  _pc 
)
inline

Definition at line 44 of file symex_target.h.

◆ sourcet() [2/4]

symex_targett::sourcet::sourcet ( const irep_idt &  _function_id,
const goto_programt &  _goto_program 
)
inlineexplicit

Definition at line 49 of file symex_target.h.

◆ sourcet() [3/4]

symex_targett::sourcet::sourcet ( sourcet &&  other)
inlinenoexcept

Definition at line 58 of file symex_target.h.

◆ sourcet() [4/4]

symex_targett::sourcet::sourcet ( const sourcet &  other)
default

Member Function Documentation

◆ operator=() [1/2]

sourcet& symex_targett::sourcet::operator= ( const sourcet &  other)
default

◆ operator=() [2/2]

sourcet& symex_targett::sourcet::operator= ( sourcet &&  other)
default

Member Data Documentation

◆ function_id

irep_idt symex_targett::sourcet::function_id

Definition at line 39 of file symex_target.h.

◆ pc

goto_programt::const_targett symex_targett::sourcet::pc

Definition at line 42 of file symex_target.h.

◆ thread_nr

unsigned symex_targett::sourcet::thread_nr

Definition at line 38 of file symex_target.h.

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