Identifies a GOTO instruction where a given variable is defined (i.e. More...
#include <reaching_definitions.h>
Collaboration diagram for reaching_definitiont:Public Member Functions | |
| reaching_definitiont (const irep_idt &identifier, const ai_domain_baset::locationt &definition_at, const range_spect &bit_begin, const range_spect &bit_end) | |
Public Attributes | |
| irep_idt | identifier |
| The name of the variable which was defined. More... | |
| ai_domain_baset::locationt | definition_at |
| The iterator to the GOTO instruction where the variable has been written to. More... | |
| range_spect | bit_begin |
| The two integers below define a range of bits (i.e. More... | |
| range_spect | bit_end |
Detailed Description
Identifies a GOTO instruction where a given variable is defined (i.e.
it is set to a certain value). It consists of these data:
Definition at line 85 of file reaching_definitions.h.
Constructor & Destructor Documentation
◆ reaching_definitiont()
|
inline |
Definition at line 98 of file reaching_definitions.h.
Member Data Documentation
◆ bit_begin
| range_spect reaching_definitiont::bit_begin |
The two integers below define a range of bits (i.e.
the begin and end bit indices) which represent the value of the variable. So, the integers represents the half-open interval [bit_begin, bit_end) of bits.
Definition at line 95 of file reaching_definitions.h.
◆ bit_end
| range_spect reaching_definitiont::bit_end |
Definition at line 96 of file reaching_definitions.h.
◆ definition_at
| ai_domain_baset::locationt reaching_definitiont::definition_at |
The iterator to the GOTO instruction where the variable has been written to.
Definition at line 91 of file reaching_definitions.h.
◆ identifier
| irep_idt reaching_definitiont::identifier |
The name of the variable which was defined.
Definition at line 88 of file reaching_definitions.h.
The documentation for this struct was generated from the following file:
- /home/runner/work/cbmc/cbmc/src/analyses/reaching_definitions.h
