cprover
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 ()
 
 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
 

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 35 of file symex_target.h.

Constructor & Destructor Documentation

◆ sourcet() [1/3]

symex_targett::sourcet::sourcet ( )
inline

Definition at line 44 of file symex_target.h.

◆ sourcet() [2/3]

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

Definition at line 48 of file symex_target.h.

◆ sourcet() [3/3]

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

Definition at line 53 of file symex_target.h.

Member Data Documentation

◆ function

irep_idt symex_targett::sourcet::function

Definition at line 38 of file symex_target.h.

◆ is_set

bool symex_targett::sourcet::is_set

Definition at line 42 of file symex_target.h.

◆ pc

goto_programt::const_targett symex_targett::sourcet::pc

Definition at line 41 of file symex_target.h.

◆ thread_nr

unsigned symex_targett::sourcet::thread_nr

Definition at line 37 of file symex_target.h.

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