CBMC
Loading...
Searching...
No Matches
Public Member Functions | Public Attributes | List of all members
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:
[フレーム]
[legend]

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:

AltStyle によって変換されたページ (->オリジナル) /