cprover
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
 
sourcetoperator= (const sourcet &other)=default
 
sourcetoperator= (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 37 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 45 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 50 of file symex_target.h.

◆ sourcet() [3/4]

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

Definition at line 59 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 40 of file symex_target.h.

◆ pc

goto_programt::const_targett symex_targett::sourcet::pc

Definition at line 43 of file symex_target.h.

◆ thread_nr

unsigned symex_targett::sourcet::thread_nr

Definition at line 39 of file symex_target.h.


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