CBMC
statement_list_typecheckt::stl_jump_locationt Struct Reference

Holds information about the properties of a jump instruction. More...

Public Member Functions

 stl_jump_locationt (size_t nesting_depth, bool sets_fc_false)
 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 sets_fc_false
 States if the jump instruction sets the /FC bit to false. More...
 

Detailed Description

Holds information about the properties of a jump instruction.

Definition at line 152 of file statement_list_typecheck.h.

Constructor & Destructor Documentation

◆ stl_jump_locationt()

statement_list_typecheckt::stl_jump_locationt::stl_jump_locationt ( size_t  nesting_depth,
bool  sets_fc_false 
)

Constructs a new location with the specified properties.

Parameters
nesting_depthScope of the jump instruction.
sets_fc_falseStates whether the jump instruction modifies the /FC bit.

Definition at line 111 of file statement_list_typecheck.cpp.

Member Data Documentation

◆ nesting_depth

const size_t statement_list_typecheckt::stl_jump_locationt::nesting_depth

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

Definition at line 159 of file statement_list_typecheck.h.

◆ sets_fc_false

const bool statement_list_typecheckt::stl_jump_locationt::sets_fc_false

States if the jump instruction sets the /FC bit to false.

Definition at line 162 of file statement_list_typecheck.h.


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