CBMC
Public Member Functions | Public Attributes | List of all members
statement_list_typecheckt::nesting_stack_entryt Struct Reference

Every time branching occurs inside of a boolean expression string in STL, the current value of the RLO and OR bits are saved and put on a separate stack. More...

+ Collaboration diagram for statement_list_typecheckt::nesting_stack_entryt:

Public Member Functions

 nesting_stack_entryt (exprt rlo_bit, bool or_bit, codet function_code)
 

Public Attributes

exprt rlo_bit
 The rlo's value when the entry was generated. More...
 
bool or_bit = false
 The OR bit's value when the entry was generated. More...
 
codet function_code
 OP code of the instruction that generated the stack entry. More...
 

Detailed Description

Every time branching occurs inside of a boolean expression string in STL, the current value of the RLO and OR bits are saved and put on a separate stack.

After returning from the branch, these values are popped and replace the current status word bits.

Definition at line 100 of file statement_list_typecheck.h.

Constructor & Destructor Documentation

◆ nesting_stack_entryt()

statement_list_typecheckt::nesting_stack_entryt::nesting_stack_entryt ( exprt  rlo_bit,
bool  or_bit,
codet  function_code 
)

Definition at line 94 of file statement_list_typecheck.cpp.

Member Data Documentation

◆ function_code

codet statement_list_typecheckt::nesting_stack_entryt::function_code

OP code of the instruction that generated the stack entry.

Definition at line 109 of file statement_list_typecheck.h.

◆ or_bit

bool statement_list_typecheckt::nesting_stack_entryt::or_bit = false

The OR bit's value when the entry was generated.

Definition at line 106 of file statement_list_typecheck.h.

◆ rlo_bit

exprt statement_list_typecheckt::nesting_stack_entryt::rlo_bit

The rlo's value when the entry was generated.

Definition at line 103 of file statement_list_typecheck.h.

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