cprover
reaching_definitiont Struct Reference

Identifies a GOTO instruction where a given variable is defined (i.e. More...

#include <reaching_definitions.h>

+ Collaboration diagram for reaching_definitiont:

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 86 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. 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.

◆ bit_end

range_spect reaching_definitiont::bit_end

Definition at line 99 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 92 of file reaching_definitions.h.

◆ identifier

irep_idt reaching_definitiont::identifier

The name of the variable which was defined.

Definition at line 89 of file reaching_definitions.h.


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