cprover
|
Identifies source in the context of symbolic execution. More...
#include <symex_target.h>
Public Member Functions | |
sourcet () | |
sourcet (const irep_idt &_function, goto_programt::const_targett _pc) | |
sourcet (const irep_idt &_function, const goto_programt &_goto_program) | |
Public Attributes | |
unsigned | thread_nr |
irep_idt | function |
goto_programt::const_targett | pc |
bool | is_set |
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 35 of file symex_target.h.
|
inline |
Definition at line 44 of file symex_target.h.
|
inline |
Definition at line 48 of file symex_target.h.
|
inlineexplicit |
Definition at line 53 of file symex_target.h.
irep_idt symex_targett::sourcet::function |
Definition at line 38 of file symex_target.h.
bool symex_targett::sourcet::is_set |
Definition at line 42 of file symex_target.h.
goto_programt::const_targett symex_targett::sourcet::pc |
Definition at line 41 of file symex_target.h.
unsigned symex_targett::sourcet::thread_nr |
Definition at line 37 of file symex_target.h.