cprover
|
Identifies a GOTO instruction where a given variable is defined (i.e. More...
#include <reaching_definitions.h>
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 |
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 86 of file reaching_definitions.h.
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. However, bit_end
can also be set a special value -1
, which means infinite/unknown index.
Definition at line 98 of file reaching_definitions.h.
range_spect reaching_definitiont::bit_end |
Definition at line 99 of file reaching_definitions.h.
ai_domain_baset::locationt reaching_definitiont::definition_at |
The iterator to the GOTO instruction where the variable has been written to.
Definition at line 92 of file reaching_definitions.h.
irep_idt reaching_definitiont::identifier |
The name of the variable which was defined.
Definition at line 89 of file reaching_definitions.h.