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 

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 

Definition at line 50 of file symex_target.h.

◆ sourcet() [3/4]

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

Definition at line 59 of file symex_target.h.

◆ sourcet() [4/4]

symex_targett::sourcet::sourcet ( const sourcet other)

Member Function Documentation

◆ operator=() [1/2]

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

◆ operator=() [2/2]

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

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: