CBMC
statement_list_typecheckt::stl_label_locationt Struct Reference

Holds information about the instruction and the nesting depth to which a label points. More...

Public Member Functions

 stl_label_locationt (size_t nesting_depth, bool jumps_permitted, bool fc_false_required)
 Constructs a new location with the specified properties. More...
 

Public Attributes

const size_t nesting_depth
 The size of the nesting stack at the label location, used for checking scope violations. More...
 
const bool jumps_permitted
 States if jumps to this location are permitted or if the location is invalid. More...
 
const bool fc_false_required
 States if jump instructions to this location need to set the /FC bit to false. More...
 

Detailed Description

Holds information about the instruction and the nesting depth to which a label points.

Definition at line 121 of file statement_list_typecheck.h.

Constructor & Destructor Documentation

◆ stl_label_locationt()

statement_list_typecheckt::stl_label_locationt::stl_label_locationt ( size_t  nesting_depth,
bool  jumps_permitted,
bool  fc_false_required 
)

Constructs a new location with the specified properties.

Parameters
nesting_depthScope of the label.
jumps_permittedStates whether jumps to the label are possible in general.
fc_false_requiredStates whether a jump instruction to this label needs to set the /FC bit.

Definition at line 102 of file statement_list_typecheck.cpp.

Member Data Documentation

◆ fc_false_required

const bool statement_list_typecheckt::stl_label_locationt::fc_false_required

States if jump instructions to this location need to set the /FC bit to false.

Definition at line 133 of file statement_list_typecheck.h.

◆ jumps_permitted

const bool statement_list_typecheckt::stl_label_locationt::jumps_permitted

States if jumps to this location are permitted or if the location is invalid.

Definition at line 129 of file statement_list_typecheck.h.

◆ nesting_depth

const size_t statement_list_typecheckt::stl_label_locationt::nesting_depth

The size of the nesting stack at the label location, used for checking scope violations.

Definition at line 125 of file statement_list_typecheck.h.


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