cprover
Loading...
Searching...
No Matches
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 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.
ai_domain_baset::locationt definition_at
 The iterator to the GOTO instruction where the variable has been written to.
range_spect bit_begin
 The two integers below define a range of bits (i.e.
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()

reaching_definitiont::reaching_definitiont ( const irep_idt & identifier,
const ai_domain_baset::locationt & definition_at,
const range_spect & bit_begin,
const range_spect & bit_end )
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: