cprover
Loading...
Searching...
No Matches
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 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: