cprover
statement_list_typecheckt Class Reference

Class for encapsulating the current state of the type check. More...

#include <statement_list_typecheck.h>

+ Inheritance diagram for statement_list_typecheckt:
+ Collaboration diagram for statement_list_typecheckt:

Classes

struct  nesting_stack_entryt
 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...
 

Public Member Functions

 statement_list_typecheckt (const statement_list_parse_treet &parse_tree, symbol_tablet &symbol_table, const std::string &module, message_handlert &message_handler)
 Creates a new instance of statement_list_typecheckt. More...
 
void typecheck () override
 Performs the actual typecheck by using the parse tree with which the object was initialized and modifies the referenced symbol table. More...
 
- Public Member Functions inherited from typecheckt
 typecheckt (message_handlert &_message_handler)
 
virtual ~typecheckt ()
 
virtual bool typecheck_main ()
 
- Public Member Functions inherited from messaget
virtual void set_message_handler (message_handlert &_message_handler)
 
message_handlertget_message_handler ()
 
 messaget ()
 
 messaget (const messaget &other)
 
messagetoperator= (const messaget &other)
 
 messaget (message_handlert &_message_handler)
 
virtual ~messaget ()
 
mstreamtget_mstream (unsigned message_level) const
 
mstreamterror () const
 
mstreamtwarning () const
 
mstreamtresult () const
 
mstreamtstatus () const
 
mstreamtstatistics () const
 
mstreamtprogress () const
 
mstreamtdebug () const
 
void conditional_output (mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
 Generate output to message_stream using output_generator if the configured verbosity is at least as high as that of message_stream. More...
 

Private Types

using nesting_stackt = std::vector< nesting_stack_entryt >
 

Private Member Functions

void typecheck_function_declaration (const statement_list_parse_treet::functiont &function)
 Performs a typecheck on a function declaration inside of the parse tree and adds symbols for it and its parameters to the symbol table. More...
 
void typecheck_function_block_declaration (const statement_list_parse_treet::function_blockt &function_block)
 Performs a typecheck on a function block declaration inside of the parse tree and adds symbols for it and its parameters to the symbol table. More...
 
void typecheck_tag_list ()
 Performs a typecheck on the tag list of the referenced parse tree and adds symbols for its contents to the symbol table. More...
 
void add_temp_rlo ()
 Adds a symbol for the RLO to the symbol table. More...
 
struct_typet create_instance_data_block_type (const statement_list_parse_treet::function_blockt &function_block)
 Creates a data block type for the given function block. More...
 
void typecheck_function_block_var_decls (const statement_list_parse_treet::var_declarationst &var_decls, struct_union_typet::componentst &components, const irep_idt &var_property)
 Performs a typecheck on a variable declaration list and saves the result to the given component element. More...
 
void typecheck_function_var_decls (const statement_list_parse_treet::var_declarationst &var_decls, code_typet::parameterst &params, const irep_idt &function_name, const irep_idt &var_property)
 Performs a typecheck on a variable declaration list and saves the result to the given component element. More...
 
void typecheck_temp_var_decls (const statement_list_parse_treet::tia_modulet &tia_module, symbolt &tia_symbol)
 Performs a typecheck on the temp variables of a TIA module and saves the result to the given symbol value. More...
 
void typecheck_statement_list_networks (const statement_list_parse_treet::tia_modulet &tia_module, symbolt &tia_symbol)
 Performs a typecheck on the networks of a TIA module and saves the result to the given symbol. More...
 
void typecheck_statement_list_instruction (const statement_list_parse_treet::instructiont &instruction, symbolt &tia_element)
 Performs a typecheck on a single instruction and saves the result to the given symbol body if necessary. More...
 
void typecheck_statement_list_load (const codet &op_code, const symbolt &tia_element)
 Performs a typecheck on a STL load instruction. More...
 
void typecheck_statement_list_transfer (const codet &op_code, symbolt &tia_element)
 Performs a typecheck on a STL transfer instruction and saves the result to the given symbol. More...
 
void typecheck_statement_list_accu_int_add (const codet &op_code)
 Performs a typecheck on a STL accumulator add instruction for integers. More...
 
void typecheck_statement_list_accu_int_sub (const codet &op_code)
 Performs a typecheck on a STL accumulator subtract instruction for integers. More...
 
void typecheck_statement_list_accu_int_div (const codet &op_code)
 Performs a typecheck on a STL accumulator divide instruction for integers. More...
 
void typecheck_statement_list_accu_int_mul (const codet &op_code)
 Performs a typecheck on a STL accumulator multiply instruction for integers. More...
 
void typecheck_statement_list_accu_int_eq (const codet &op_code)
 Performs a typecheck on a STL accumulator equality comparison instruction for integers. More...
 
void typecheck_statement_list_accu_int_neq (const codet &op_code)
 Performs a typecheck on a STL accumulator inequality comparison instruction for integers. More...
 
void typecheck_statement_list_accu_int_gt (const codet &op_code)
 Performs a typecheck on a STL accumulator greater than comparison instruction for integers. More...
 
void typecheck_statement_list_accu_int_lt (const codet &op_code)
 Performs a typecheck on a STL accumulator less than comparison instruction for integers. More...
 
void typecheck_statement_list_accu_int_gte (const codet &op_code)
 Performs a typecheck on a STL accumulator greater than or equal comparison instruction for integers. More...
 
void typecheck_statement_list_accu_int_lte (const codet &op_code)
 Performs a typecheck on a STL accumulator less than or equal comparison instruction for integers. More...
 
void typecheck_statement_list_accu_dint_add (const codet &op_code)
 Performs a typecheck on a STL accumulator add instruction for double integers. More...
 
void typecheck_statement_list_accu_dint_sub (const codet &op_code)
 Performs a typecheck on a STL accumulator subtract instruction for double integers. More...
 
void typecheck_statement_list_accu_dint_div (const codet &op_code)
 Performs a typecheck on a STL accumulator divide instruction for double integers. More...
 
void typecheck_statement_list_accu_dint_mul (const codet &op_code)
 Performs a typecheck on a STL accumulator divide instruction for double integers. More...
 
void typecheck_statement_list_accu_dint_eq (const codet &op_code)
 Performs a typecheck on a STL accumulator equality comparison instruction for double integers. More...
 
void typecheck_statement_list_accu_dint_neq (const codet &op_code)
 Performs a typecheck on a STL accumulator inequality comparison instruction for double integers. More...
 
void typecheck_statement_list_accu_dint_gt (const codet &op_code)
 Performs a typecheck on a STL accumulator greater than comparison instruction for double integers. More...
 
void typecheck_statement_list_accu_dint_lt (const codet &op_code)
 Performs a typecheck on a STL accumulator less than comparison instruction for double integers. More...
 
void typecheck_statement_list_accu_dint_gte (const codet &op_code)
 Performs a typecheck on a STL accumulator greater than or equal comparison instruction for double integers. More...
 
void typecheck_statement_list_accu_dint_lte (const codet &op_code)
 Performs a typecheck on a STL accumulator less than or equal comparison instruction for double integers. More...
 
void typecheck_statement_list_accu_real_add (const codet &op_code)
 Performs a typecheck on a STL accumulator add instruction for reals. More...
 
void typecheck_statement_list_accu_real_sub (const codet &op_code)
 Performs a typecheck on a STL accumulator subtract instruction for reals. More...
 
void typecheck_statement_list_accu_real_div (const codet &op_code)
 Performs a typecheck on a STL accumulator divide instruction for reals. More...
 
void typecheck_statement_list_accu_real_mul (const codet &op_code)
 Performs a typecheck on a STL accumulator multiply instruction for reals. More...
 
void typecheck_statement_list_accu_real_eq (const codet &op_code)
 Performs a typecheck on a STL accumulator equality comparison instruction for double integers. More...
 
void typecheck_statement_list_accu_real_neq (const codet &op_code)
 Performs a typecheck on a STL accumulator inequality comparison instruction for double integers. More...
 
void typecheck_statement_list_accu_real_gt (const codet &op_code)
 Performs a typecheck on a STL accumulator greater than comparison instruction for double integers. More...
 
void typecheck_statement_list_accu_real_lt (const codet &op_code)
 Performs a typecheck on a STL accumulator less than comparison instruction for double integers. More...
 
void typecheck_statement_list_accu_real_gte (const codet &op_code)
 Performs a typecheck on a STL accumulator greater than or equal comparison instruction for double integers. More...
 
void typecheck_statement_list_accu_real_lte (const codet &op_code)
 Performs a typecheck on a STL accumulator less than or equal comparison instruction for integers. More...
 
void typecheck_statement_list_not (const codet &op_code)
 Performs a typecheck on a STL boolean NOT instruction. More...
 
void typecheck_statement_list_and (const codet &op_code, const symbolt &tia_element)
 Performs a typecheck on a STL boolean And instruction. More...
 
void typecheck_statement_list_or (const codet &op_code, const symbolt &tia_element)
 Performs a typecheck on a STL boolean Or instruction. More...
 
void typecheck_statement_list_xor (const codet &op_code, const symbolt &tia_element)
 Performs a typecheck on a STL boolean XOR instruction. More...
 
void typecheck_statement_list_and_not (const codet &op_code, const symbolt &tia_element)
 Performs a typecheck on a STL boolean And Not instruction. More...
 
void typecheck_statement_list_or_not (const codet &op_code, const symbolt &tia_element)
 Performs a typecheck on a STL boolean Or Not instruction. More...
 
void typecheck_statement_list_xor_not (const codet &op_code, const symbolt &tia_element)
 Performs a typecheck on a STL boolean XOR Not instruction. More...
 
void typecheck_statement_list_and_before_or ()
 Performs a typecheck on a STL operand-less Or instruction. More...
 
void typecheck_statement_list_nested_and (const codet &op_code)
 Performs a typecheck on a nested And instruction. More...
 
void typecheck_statement_list_nested_or (const codet &op_code)
 Performs a typecheck on a nested Or instruction. More...
 
void typecheck_statement_list_nested_xor (const codet &op_code)
 Performs a typecheck on a nested XOR instruction. More...
 
void typecheck_statement_list_nested_and_not (const codet &op_code)
 Performs a typecheck on a nested And Not instruction. More...
 
void typecheck_statement_list_nested_or_not (const codet &op_code)
 Performs a typecheck on a nested Or Not instruction. More...
 
void typecheck_statement_list_nested_xor_not (const codet &op_code)
 Performs a typecheck on a nested XOR Not instruction. More...
 
void typecheck_statement_list_nesting_closed (const codet &op_code)
 Performs a typecheck on a Nesting Closed instruction. More...
 
void typecheck_statement_list_assign (const codet &op_code, symbolt &tia_element)
 Performs a typecheck on a STL assign instruction and saves the result to the given symbol. More...
 
void typecheck_statement_list_set_rlo (const codet &op_code)
 Performs a typecheck on a STL 'SET' instruction and modifies the RLO, OR and FC bit. More...
 
void typecheck_statement_list_clr_rlo (const codet &op_code)
 Performs a typecheck on a STL 'CLR' instruction and modifies the RLO, OR and FC bit. More...
 
void typecheck_statement_list_set (const codet &op_code, symbolt &tia_element)
 Performs a typecheck on a STL 'S' instruction and saves the result to the given symbol. More...
 
void typecheck_statement_list_reset (const codet &op_code, symbolt &tia_element)
 Performs a typecheck on a STL 'R' instruction and saves the result to the given symbol. More...
 
void typecheck_statement_list_call (const codet &op_code, symbolt &tia_element)
 Performs a typecheck on a STL Call instruction and saves the result to the given symbol. More...
 
void typecheck_statement_list_accu_int_arith (const codet &op_code)
 Performs a typecheck on a STL Accumulator instruction for integers. More...
 
void typecheck_statement_list_accu_dint_arith (const codet &op_code)
 Performs a typecheck on a STL Accumulator instruction for double integers. More...
 
void typecheck_statement_list_accu_real_arith (const codet &op_code)
 Performs a typecheck on a STL Accumulator instruction for reals. More...
 
const symbol_exprttypecheck_instruction_with_non_const_operand (const codet &op_code)
 Performs a typecheck on a STL instruction with an additional operand that should be no constant. More...
 
void typecheck_instruction_without_operand (const codet &op_code)
 Performs a typecheck on an operand-less STL instruction. More...
 
void typecheck_binary_accumulator_instruction (const codet &op_code)
 Performs a typecheck on a STL instruction that uses two accumulator entries. More...
 
void typecheck_nested_boolean_instruction (const codet &op_code, const exprt &rlo_value)
 Performs a typecheck on a STL instruction that initializes a new boolean nesting. More...
 
exprt typecheck_simple_boolean_instruction_operand (const codet &op_code, const symbolt &tia_element, bool negate)
 Performs a typecheck on the operand of a not nested boolean instruction and returns the result. More...
 
void typecheck_accumulator_compare_instruction (const irep_idt &comparison)
 Performs a typecheck on an STL comparison instruction. More...
 
exprt typecheck_identifier (const symbolt &tia_element, const irep_idt &identifier)
 Performs a typecheck on the given identifier and returns its symbol. More...
 
void typecheck_CPROVER_assert (const codet &op_code, symbolt &tia_element)
 Performs a typecheck on a call of __CPOVER_ASSERT and saves the result to the given symbol. More...
 
void typecheck_CPROVER_assume (const codet &op_code, symbolt &tia_element)
 Performs a typecheck on a call of __CPOVER_ASSUME and saves the result to the given symbol. More...
 
void typecheck_called_tia_element (const codet &op_code, symbolt &tia_element)
 Performs a typecheck on a call of a TIA element and saves the result to the given symbol. More...
 
void typecheck_called_function (const codet &op_code, symbolt &tia_element)
 Performs a typecheck on a call of a TIA function and saves the result to the given symbol. More...
 
void typecheck_called_function_block (const codet &op_code, symbolt &tia_element)
 Performs a typecheck on a call of a TIA function block and saves the result to the given symbol. More...
 
exprt typecheck_function_call_arguments (const std::vector< equal_exprt > &assignments, const code_typet::parametert &param, const symbolt &tia_element)
 Checks if the given parameter is inside of the assignment list of a function call and returns the expression of the assigned variable. More...
 
exprt typecheck_function_call_argument_rhs (const symbolt &tia_element, const exprt &rhs)
 Checks if the given assigned expression is a variable or a constant and returns the typechecked version. More...
 
exprt typecheck_return_value_assignment (const std::vector< equal_exprt > &assignments, const typet &return_type, const symbolt &tia_element)
 Checks if there is a return value assignment inside of the assignment list of a function call and returns the expression of the assigned variable. More...
 
void add_to_or_rlo_wrapper (const exprt &op)
 Adds the given expression to the operands of the Or expression that is saved in the RLO. More...
 
void initialize_bit_expression (const exprt &op)
 Initializes the FC, RLO an OR bits for the scenario when a new boolean instruction was encontered. More...
 
void save_rlo_state (symbolt &tia_element)
 Saves the current RLO bit to a temporary variable to prevent false overrides when modifying boolean variables. More...
 

Private Attributes

const statement_list_parse_treetparse_tree
 Parse tree which is used to fill the symbol table. More...
 
symbol_tabletsymbol_table
 Reference to the symbol table that should be filled during the typecheck. More...
 
const irep_idt module
 Name of the module this typecheck belongs to. More...
 
std::vector< exprtaccumulator
 Representation of the accumulator of a TIA element. More...
 
exprt rlo_bit = true_exprt()
 Result of Logic Operation (Part of the TIA status word). More...
 
bool fc_bit = false
 First Check (Part of the TIA status word). More...
 
bool or_bit = false
 Or (Part of the TIA status word). More...
 
nesting_stackt nesting_stack
 Representation of the nesting stack. More...
 

Additional Inherited Members

- Public Types inherited from messaget
enum  message_levelt {
  M_ERROR =1, M_WARNING =2, M_RESULT =4, M_STATUS =6,
  M_STATISTICS =8, M_PROGRESS =9, M_DEBUG =10
}
 
- Static Public Member Functions inherited from messaget
static unsigned eval_verbosity (const std::string &user_input, const message_levelt default_verbosity, message_handlert &dest)
 Parse a (user-)provided string as a verbosity level and set it as the verbosity of dest. More...
 
static commandt command (unsigned c)
 Create an ECMA-48 SGR (Select Graphic Rendition) command. More...
 
- Static Public Attributes inherited from messaget
static eomt eom
 
static const commandt reset
 return to default formatting, as defined by the terminal More...
 
static const commandt red
 render text with red foreground color More...
 
static const commandt green
 render text with green foreground color More...
 
static const commandt yellow
 render text with yellow foreground color More...
 
static const commandt blue
 render text with blue foreground color More...
 
static const commandt magenta
 render text with magenta foreground color More...
 
static const commandt cyan
 render text with cyan foreground color More...
 
static const commandt bright_red
 render text with bright red foreground color More...
 
static const commandt bright_green
 render text with bright green foreground color More...
 
static const commandt bright_yellow
 render text with bright yellow foreground color More...
 
static const commandt bright_blue
 render text with bright blue foreground color More...
 
static const commandt bright_magenta
 render text with bright magenta foreground color More...
 
static const commandt bright_cyan
 render text with bright cyan foreground color More...
 
static const commandt bold
 render text with bold font More...
 
static const commandt faint
 render text with faint font More...
 
static const commandt italic
 render italic text More...
 
static const commandt underline
 render underlined text More...
 
- Protected Attributes inherited from messaget
message_handlertmessage_handler
 
mstreamt mstream
 

Detailed Description

Class for encapsulating the current state of the type check.

Definition at line 37 of file statement_list_typecheck.h.

Member Typedef Documentation

◆ nesting_stackt

Definition at line 108 of file statement_list_typecheck.h.

Constructor & Destructor Documentation

◆ statement_list_typecheckt()

statement_list_typecheckt::statement_list_typecheckt ( const statement_list_parse_treet parse_tree,
symbol_tablet symbol_table,
const std::string &  module,
message_handlert message_handler 
)

Creates a new instance of statement_list_typecheckt.

Parameters
parse_treeParse tree generated by parsing a Statement List file.
[out]symbol_tableObject that shall be filled by this function. If the symbol table is not empty when calling this function, its contents are merged with the new entries.
moduleName of the file that has been parsed.
message_handlerUsed to provide debug information and error messages.

Definition at line 77 of file statement_list_typecheck.cpp.

Member Function Documentation

◆ add_temp_rlo()

void statement_list_typecheckt::add_temp_rlo ( )
private

Adds a symbol for the RLO to the symbol table.

This symbol is used by other operations to save intermediate results of the rlo expression.

Definition at line 204 of file statement_list_typecheck.cpp.

◆ add_to_or_rlo_wrapper()

void statement_list_typecheckt::add_to_or_rlo_wrapper ( const exprt op)
private

Adds the given expression to the operands of the Or expression that is saved in the RLO.

Parameters
opOperand to be added to the Or instruction.

Definition at line 1499 of file statement_list_typecheck.cpp.

◆ create_instance_data_block_type()

struct_typet statement_list_typecheckt::create_instance_data_block_type ( const statement_list_parse_treet::function_blockt function_block)
private

Creates a data block type for the given function block.

Parameters
function_blockFunction block with an interface that should be converted to a data block.
Returns
: A type representation of an instance data block for the function block.

Definition at line 217 of file statement_list_typecheck.cpp.

◆ initialize_bit_expression()

void statement_list_typecheckt::initialize_bit_expression ( const exprt op)
private

Initializes the FC, RLO an OR bits for the scenario when a new boolean instruction was encontered.

Parameters
opOperand of the encountered instruction.

Definition at line 1519 of file statement_list_typecheck.cpp.

◆ save_rlo_state()

void statement_list_typecheckt::save_rlo_state ( symbolt tia_element)
private

Saves the current RLO bit to a temporary variable to prevent false overrides when modifying boolean variables.

Parameters
tia_elementSymbol representation of the TIA element.

Definition at line 1526 of file statement_list_typecheck.cpp.

◆ typecheck()

void statement_list_typecheckt::typecheck ( )
overridevirtual

Performs the actual typecheck by using the parse tree with which the object was initialized and modifies the referenced symbol table.

Implements typecheckt.

Definition at line 89 of file statement_list_typecheck.cpp.

◆ typecheck_accumulator_compare_instruction()

void statement_list_typecheckt::typecheck_accumulator_compare_instruction ( const irep_idt comparison)
private

Performs a typecheck on an STL comparison instruction.

Modifies the RLO.

Parameters
comparisonID of the compare expression that should be pushed to the RLO.

Definition at line 1174 of file statement_list_typecheck.cpp.

◆ typecheck_binary_accumulator_instruction()

void statement_list_typecheckt::typecheck_binary_accumulator_instruction ( const codet op_code)
private

Performs a typecheck on a STL instruction that uses two accumulator entries.

Parameters
op_codeOP code of the instruction.

Definition at line 1208 of file statement_list_typecheck.cpp.

◆ typecheck_called_function()

void statement_list_typecheckt::typecheck_called_function ( const codet op_code,
symbolt tia_element 
)
private

Performs a typecheck on a call of a TIA function and saves the result to the given symbol.

Parameters
op_codeOP code of the instruction.
[out]tia_elementSymbol representation of the TIA element.

Definition at line 1369 of file statement_list_typecheck.cpp.

◆ typecheck_called_function_block()

void statement_list_typecheckt::typecheck_called_function_block ( const codet op_code,
symbolt tia_element 
)
private

Performs a typecheck on a call of a TIA function block and saves the result to the given symbol.

Parameters
op_codeOP code of the instruction.
[out]tia_elementSymbol representation of the TIA element.

Definition at line 1413 of file statement_list_typecheck.cpp.

◆ typecheck_called_tia_element()

void statement_list_typecheckt::typecheck_called_tia_element ( const codet op_code,
symbolt tia_element 
)
private

Performs a typecheck on a call of a TIA element and saves the result to the given symbol.

Parameters
op_codeOP code of the instruction.
[out]tia_elementSymbol representation of the TIA element.

Definition at line 1347 of file statement_list_typecheck.cpp.

◆ typecheck_CPROVER_assert()

void statement_list_typecheckt::typecheck_CPROVER_assert ( const codet op_code,
symbolt tia_element 
)
private

Performs a typecheck on a call of __CPOVER_ASSERT and saves the result to the given symbol.

Parameters
op_codeOP code of the instruction.
[out]tia_elementSymbol representation of the TIA element.

Definition at line 1309 of file statement_list_typecheck.cpp.

◆ typecheck_CPROVER_assume()

void statement_list_typecheckt::typecheck_CPROVER_assume ( const codet op_code,
symbolt tia_element 
)
private

Performs a typecheck on a call of __CPOVER_ASSUME and saves the result to the given symbol.

Parameters
op_codeOP code of the instruction.
[out]tia_elementSymbol representation of the TIA element.

Definition at line 1328 of file statement_list_typecheck.cpp.

◆ typecheck_function_block_declaration()

void statement_list_typecheckt::typecheck_function_block_declaration ( const statement_list_parse_treet::function_blockt function_block)
private

Performs a typecheck on a function block declaration inside of the parse tree and adds symbols for it and its parameters to the symbol table.

Parameters
function_blockFunction block to be checked.

Definition at line 116 of file statement_list_typecheck.cpp.

◆ typecheck_function_block_var_decls()

void statement_list_typecheckt::typecheck_function_block_var_decls ( const statement_list_parse_treet::var_declarationst var_decls,
struct_union_typet::componentst components,
const irep_idt var_property 
)
private

Performs a typecheck on a variable declaration list and saves the result to the given component element.

Parameters
var_declsList of declarations which should be typechecked.
[out]componentsList of typechecked and converted declarations.
var_propertyType of variable declaration list (for example input, output, ...).

Definition at line 233 of file statement_list_typecheck.cpp.

◆ typecheck_function_call_argument_rhs()

exprt statement_list_typecheckt::typecheck_function_call_argument_rhs ( const symbolt tia_element,
const exprt rhs 
)
private

Checks if the given assigned expression is a variable or a constant and returns the typechecked version.

Parameters
tia_elementSymbol representation of the TIA element.
rhsExpression that the function parameter got assigned to.
Returns
: Expression of either a symbol or a constant.

Definition at line 1456 of file statement_list_typecheck.cpp.

◆ typecheck_function_call_arguments()

exprt statement_list_typecheckt::typecheck_function_call_arguments ( const std::vector< equal_exprt > &  assignments,
const code_typet::parametert param,
const symbolt tia_element 
)
private

Checks if the given parameter is inside of the assignment list of a function call and returns the expression of the assigned variable.

Parameters
assignmentsAssignment list of the function call.
paramParameter that should be checked.
tia_elementSymbol representation of the TIA element.
Returns
: Expression including the assigned symbol's name and type.

Definition at line 1425 of file statement_list_typecheck.cpp.

◆ typecheck_function_declaration()

void statement_list_typecheckt::typecheck_function_declaration ( const statement_list_parse_treet::functiont function)
private

Performs a typecheck on a function declaration inside of the parse tree and adds symbols for it and its parameters to the symbol table.

Parameters
functionFunction to be checked.

Definition at line 165 of file statement_list_typecheck.cpp.

◆ typecheck_function_var_decls()

void statement_list_typecheckt::typecheck_function_var_decls ( const statement_list_parse_treet::var_declarationst var_decls,
code_typet::parameterst params,
const irep_idt function_name,
const irep_idt var_property 
)
private

Performs a typecheck on a variable declaration list and saves the result to the given component element.

Parameters
var_declsList of declarations which should be typechecked.
[out]paramsList of typechecked and converted declarations.
function_nameFunction to which the variable list belongs (used for naming).
var_propertyType of variable declaration list (for example input, output, ...).

Definition at line 249 of file statement_list_typecheck.cpp.

◆ typecheck_identifier()

exprt statement_list_typecheckt::typecheck_identifier ( const symbolt tia_element,
const irep_idt identifier 
)
private

Performs a typecheck on the given identifier and returns its symbol.

Parameters
identifierIdentifier that should be checked.
tia_elementSymbol representation of the current TIA module.
Returns
: Expression including the symbol's name and type.

Definition at line 1247 of file statement_list_typecheck.cpp.

◆ typecheck_instruction_with_non_const_operand()

const symbol_exprt & statement_list_typecheckt::typecheck_instruction_with_non_const_operand ( const codet op_code)
private

Performs a typecheck on a STL instruction with an additional operand that should be no constant.

Parameters
op_codeOP code of the instruction.
Returns
: Reference to the operand.

Definition at line 1185 of file statement_list_typecheck.cpp.

◆ typecheck_instruction_without_operand()

void statement_list_typecheckt::typecheck_instruction_without_operand ( const codet op_code)
private

Performs a typecheck on an operand-less STL instruction.

Parameters
op_codeOP code of the instruction.

Definition at line 1198 of file statement_list_typecheck.cpp.

◆ typecheck_nested_boolean_instruction()

void statement_list_typecheckt::typecheck_nested_boolean_instruction ( const codet op_code,
const exprt rlo_value 
)
private

Performs a typecheck on a STL instruction that initializes a new boolean nesting.

Parameters
op_codeOP code of the instruction.
rlo_valueValue of the RLO that is pushed on the nesting stack for the case that this is the first instruction of a new bit string.

Definition at line 1219 of file statement_list_typecheck.cpp.

◆ typecheck_return_value_assignment()

exprt statement_list_typecheckt::typecheck_return_value_assignment ( const std::vector< equal_exprt > &  assignments,
const typet return_type,
const symbolt tia_element 
)
private

Checks if there is a return value assignment inside of the assignment list of a function call and returns the expression of the assigned variable.

Parameters
assignmentsAssignment list of the function call.
return_typeType of the return value.
tia_elementSymbol representation of the TIA element.
Returns
: Expression including the assigned symbol's name and type.

Definition at line 1471 of file statement_list_typecheck.cpp.

◆ typecheck_simple_boolean_instruction_operand()

exprt statement_list_typecheckt::typecheck_simple_boolean_instruction_operand ( const codet op_code,
const symbolt tia_element,
bool  negate 
)
private

Performs a typecheck on the operand of a not nested boolean instruction and returns the result.

Parameters
op_codeOP code of the instruction.
tia_elementSymbol representation of the TIA element.
negateWhether the operand should be negated (e.g. for the AND NOT expression).
Returns
: Typechecked operand.

Definition at line 1235 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_accu_dint_add()

void statement_list_typecheckt::typecheck_statement_list_accu_dint_add ( const codet op_code)
private

Performs a typecheck on a STL accumulator add instruction for double integers.

Modifies the accumulator.

Parameters
op_codeOP code of the instruction.

Definition at line 570 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_accu_dint_arith()

void statement_list_typecheckt::typecheck_statement_list_accu_dint_arith ( const codet op_code)
private

Performs a typecheck on a STL Accumulator instruction for double integers.

Parameters
op_codeOP code of the instruction.

Definition at line 1136 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_accu_dint_div()

void statement_list_typecheckt::typecheck_statement_list_accu_dint_div ( const codet op_code)
private

Performs a typecheck on a STL accumulator divide instruction for double integers.

Modifies the accumulator.

Parameters
op_codeOP code of the instruction.

Definition at line 609 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_accu_dint_eq()

void statement_list_typecheckt::typecheck_statement_list_accu_dint_eq ( const codet op_code)
private

Performs a typecheck on a STL accumulator equality comparison instruction for double integers.

Modifies the RLO.

Parameters
op_codeOP code of the instruction.

Definition at line 622 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_accu_dint_gt()

void statement_list_typecheckt::typecheck_statement_list_accu_dint_gt ( const codet op_code)
private

Performs a typecheck on a STL accumulator greater than comparison instruction for double integers.

Modifies the RLO.

Parameters
op_codeOP code of the instruction.

Definition at line 643 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_accu_dint_gte()

void statement_list_typecheckt::typecheck_statement_list_accu_dint_gte ( const codet op_code)
private

Performs a typecheck on a STL accumulator greater than or equal comparison instruction for double integers.

Modifies the RLO.

Parameters
op_codeOP code of the instruction.

Definition at line 657 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_accu_dint_lt()

void statement_list_typecheckt::typecheck_statement_list_accu_dint_lt ( const codet op_code)
private

Performs a typecheck on a STL accumulator less than comparison instruction for double integers.

Modifies the RLO.

Parameters
op_codeOP code of the instruction.

Definition at line 636 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_accu_dint_lte()

void statement_list_typecheckt::typecheck_statement_list_accu_dint_lte ( const codet op_code)
private

Performs a typecheck on a STL accumulator less than or equal comparison instruction for double integers.

Modifies the RLO.

Parameters
op_codeOP code of the instruction.

Definition at line 650 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_accu_dint_mul()

void statement_list_typecheckt::typecheck_statement_list_accu_dint_mul ( const codet op_code)
private

Performs a typecheck on a STL accumulator divide instruction for double integers.

Modifies the accumulator.

Parameters
op_codeOP code of the instruction.

Definition at line 596 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_accu_dint_neq()

void statement_list_typecheckt::typecheck_statement_list_accu_dint_neq ( const codet op_code)
private

Performs a typecheck on a STL accumulator inequality comparison instruction for double integers.

Modifies the RLO.

Parameters
op_codeOP code of the instruction.

Definition at line 629 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_accu_dint_sub()

void statement_list_typecheckt::typecheck_statement_list_accu_dint_sub ( const codet op_code)
private

Performs a typecheck on a STL accumulator subtract instruction for double integers.

Modifies the accumulator.

Parameters
op_codeOP code of the instruction.

Definition at line 583 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_accu_int_add()

void statement_list_typecheckt::typecheck_statement_list_accu_int_add ( const codet op_code)
private

Performs a typecheck on a STL accumulator add instruction for integers.

Modifies the accumulator.

Parameters
op_codeOP code of the instruction.

Definition at line 476 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_accu_int_arith()

void statement_list_typecheckt::typecheck_statement_list_accu_int_arith ( const codet op_code)
private

Performs a typecheck on a STL Accumulator instruction for integers.

Parameters
op_codeOP code of the instruction.

Definition at line 1115 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_accu_int_div()

void statement_list_typecheckt::typecheck_statement_list_accu_int_div ( const codet op_code)
private

Performs a typecheck on a STL accumulator divide instruction for integers.

Modifies the accumulator.

Parameters
op_codeOP code of the instruction.

Definition at line 515 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_accu_int_eq()

void statement_list_typecheckt::typecheck_statement_list_accu_int_eq ( const codet op_code)
private

Performs a typecheck on a STL accumulator equality comparison instruction for integers.

Modifies the RLO.

Parameters
op_codeOP code of the instruction.

Definition at line 528 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_accu_int_gt()

void statement_list_typecheckt::typecheck_statement_list_accu_int_gt ( const codet op_code)
private

Performs a typecheck on a STL accumulator greater than comparison instruction for integers.

Modifies the RLO.

Parameters
op_codeOP code of the instruction.

Definition at line 549 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_accu_int_gte()

void statement_list_typecheckt::typecheck_statement_list_accu_int_gte ( const codet op_code)
private

Performs a typecheck on a STL accumulator greater than or equal comparison instruction for integers.

Modifies the RLO.

Parameters
op_codeOP code of the instruction.

Definition at line 563 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_accu_int_lt()

void statement_list_typecheckt::typecheck_statement_list_accu_int_lt ( const codet op_code)
private

Performs a typecheck on a STL accumulator less than comparison instruction for integers.

Modifies the RLO.

Parameters
op_codeOP code of the instruction.

Definition at line 542 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_accu_int_lte()

void statement_list_typecheckt::typecheck_statement_list_accu_int_lte ( const codet op_code)
private

Performs a typecheck on a STL accumulator less than or equal comparison instruction for integers.

Modifies the RLO.

Parameters
op_codeOP code of the instruction.

Definition at line 556 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_accu_int_mul()

void statement_list_typecheckt::typecheck_statement_list_accu_int_mul ( const codet op_code)
private

Performs a typecheck on a STL accumulator multiply instruction for integers.

Modifies the accumulator.

Parameters
op_codeOP code of the instruction.

Definition at line 502 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_accu_int_neq()

void statement_list_typecheckt::typecheck_statement_list_accu_int_neq ( const codet op_code)
private

Performs a typecheck on a STL accumulator inequality comparison instruction for integers.

Modifies the RLO.

Parameters
op_codeOP code of the instruction.

Definition at line 535 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_accu_int_sub()

void statement_list_typecheckt::typecheck_statement_list_accu_int_sub ( const codet op_code)
private

Performs a typecheck on a STL accumulator subtract instruction for integers.

Modifies the accumulator.

Parameters
op_codeOP code of the instruction.

Definition at line 489 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_accu_real_add()

void statement_list_typecheckt::typecheck_statement_list_accu_real_add ( const codet op_code)
private

Performs a typecheck on a STL accumulator add instruction for reals.

Modifies the accumulator.

Parameters
op_codeOP code of the instruction.

Definition at line 664 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_accu_real_arith()

void statement_list_typecheckt::typecheck_statement_list_accu_real_arith ( const codet op_code)
private

Performs a typecheck on a STL Accumulator instruction for reals.

Parameters
op_codeOP code of the instruction.

Definition at line 1158 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_accu_real_div()

void statement_list_typecheckt::typecheck_statement_list_accu_real_div ( const codet op_code)
private

Performs a typecheck on a STL accumulator divide instruction for reals.

Modifies the accumulator.

Parameters
op_codeOP code of the instruction.

Definition at line 703 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_accu_real_eq()

void statement_list_typecheckt::typecheck_statement_list_accu_real_eq ( const codet op_code)
private

Performs a typecheck on a STL accumulator equality comparison instruction for double integers.

Modifies the RLO.

Parameters
op_codeOP code of the instruction.

Definition at line 716 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_accu_real_gt()

void statement_list_typecheckt::typecheck_statement_list_accu_real_gt ( const codet op_code)
private

Performs a typecheck on a STL accumulator greater than comparison instruction for double integers.

Modifies the RLO.

Parameters
op_codeOP code of the instruction.

Definition at line 737 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_accu_real_gte()

void statement_list_typecheckt::typecheck_statement_list_accu_real_gte ( const codet op_code)
private

Performs a typecheck on a STL accumulator greater than or equal comparison instruction for double integers.

Modifies the RLO.

Parameters
op_codeOP code of the instruction.

Definition at line 751 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_accu_real_lt()

void statement_list_typecheckt::typecheck_statement_list_accu_real_lt ( const codet op_code)
private

Performs a typecheck on a STL accumulator less than comparison instruction for double integers.

Modifies the RLO.

Parameters
op_codeOP code of the instruction.

Definition at line 730 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_accu_real_lte()

void statement_list_typecheckt::typecheck_statement_list_accu_real_lte ( const codet op_code)
private

Performs a typecheck on a STL accumulator less than or equal comparison instruction for integers.

Modifies the RLO.

Parameters
op_codeOP code of the instruction.

Definition at line 744 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_accu_real_mul()

void statement_list_typecheckt::typecheck_statement_list_accu_real_mul ( const codet op_code)
private

Performs a typecheck on a STL accumulator multiply instruction for reals.

Modifies the accumulator.

Parameters
op_codeOP code of the instruction.

Definition at line 690 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_accu_real_neq()

void statement_list_typecheckt::typecheck_statement_list_accu_real_neq ( const codet op_code)
private

Performs a typecheck on a STL accumulator inequality comparison instruction for double integers.

Modifies the RLO.

Parameters
op_codeOP code of the instruction.

Definition at line 723 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_accu_real_sub()

void statement_list_typecheckt::typecheck_statement_list_accu_real_sub ( const codet op_code)
private

Performs a typecheck on a STL accumulator subtract instruction for reals.

Modifies the accumulator.

Parameters
op_codeOP code of the instruction.

Definition at line 677 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_and()

void statement_list_typecheckt::typecheck_statement_list_and ( const codet op_code,
const symbolt tia_element 
)
private

Performs a typecheck on a STL boolean And instruction.

Reads and modifies the RLO, OR and FC bit.

Parameters
op_codeOP code of the instruction.
tia_elementSymbol representation of the TIA element.

Definition at line 772 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_and_before_or()

void statement_list_typecheckt::typecheck_statement_list_and_before_or ( )
private

Performs a typecheck on a STL operand-less Or instruction.

Reads and modifies the RLO, OR and FC bit.

Definition at line 903 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_and_not()

void statement_list_typecheckt::typecheck_statement_list_and_not ( const codet op_code,
const symbolt tia_element 
)
private

Performs a typecheck on a STL boolean And Not instruction.

Reads and modifies the RLO, OR and FC bit.

Parameters
op_codeOP code of the instruction.
tia_elementSymbol representation of the TIA element.

Definition at line 794 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_assign()

void statement_list_typecheckt::typecheck_statement_list_assign ( const codet op_code,
symbolt tia_element 
)
private

Performs a typecheck on a STL assign instruction and saves the result to the given symbol.

Modifies the RLO, OR and FC bit.

Parameters
op_codeOP code of the instruction.
[out]tia_elementSymbol representation of the TIA element.

Definition at line 1021 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_call()

void statement_list_typecheckt::typecheck_statement_list_call ( const codet op_code,
symbolt tia_element 
)
private

Performs a typecheck on a STL Call instruction and saves the result to the given symbol.

Modifies the OR and FC bit.

Parameters
op_codeOP code of the instruction.
[out]tia_elementSymbol representation of the TIA element.

Definition at line 1094 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_clr_rlo()

void statement_list_typecheckt::typecheck_statement_list_clr_rlo ( const codet op_code)
private

Performs a typecheck on a STL 'CLR' instruction and modifies the RLO, OR and FC bit.

Parameters
op_codeOP code of the instruction.

Definition at line 1051 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_instruction()

void statement_list_typecheckt::typecheck_statement_list_instruction ( const statement_list_parse_treet::instructiont instruction,
symbolt tia_element 
)
private

Performs a typecheck on a single instruction and saves the result to the given symbol body if necessary.

Parameters
instructionInstruction that should be checked.
[out]tia_elementSymbol representation of the TIA module.

Definition at line 319 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_load()

void statement_list_typecheckt::typecheck_statement_list_load ( const codet op_code,
const symbolt tia_element 
)
private

Performs a typecheck on a STL load instruction.

Modifies the accumulator.

Parameters
op_codeOP code of the instruction.
tia_elementSymbol representation of the TIA element.

Definition at line 440 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_nested_and()

void statement_list_typecheckt::typecheck_statement_list_nested_and ( const codet op_code)
private

Performs a typecheck on a nested And instruction.

Pushes the current program state to the nesting stack and cleans the RLO, OR and FC bit.

Parameters
op_codeOP code of the instruction.

Definition at line 914 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_nested_and_not()

void statement_list_typecheckt::typecheck_statement_list_nested_and_not ( const codet op_code)
private

Performs a typecheck on a nested And Not instruction.

Pushes the current program state to the nesting stack and cleans the RLO, OR and FC bit.

Parameters
op_codeOP code of the instruction.

Definition at line 922 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_nested_or()

void statement_list_typecheckt::typecheck_statement_list_nested_or ( const codet op_code)
private

Performs a typecheck on a nested Or instruction.

Pushes the current program state to the nesting stack and cleans the RLO, OR and FC bit.

Parameters
op_codeOP code of the instruction.

Definition at line 930 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_nested_or_not()

void statement_list_typecheckt::typecheck_statement_list_nested_or_not ( const codet op_code)
private

Performs a typecheck on a nested Or Not instruction.

Pushes the current program state to the nesting stack and cleans the RLO, OR and FC bit.

Parameters
op_codeOP code of the instruction.

Definition at line 938 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_nested_xor()

void statement_list_typecheckt::typecheck_statement_list_nested_xor ( const codet op_code)
private

Performs a typecheck on a nested XOR instruction.

Pushes the current program state to the nesting stack and cleans the RLO, OR and FC bit.

Parameters
op_codeOP code of the instruction.

Definition at line 946 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_nested_xor_not()

void statement_list_typecheckt::typecheck_statement_list_nested_xor_not ( const codet op_code)
private

Performs a typecheck on a nested XOR Not instruction.

Pushes the current program state to the nesting stack and cleans the RLO, OR and FC bit.

Parameters
op_codeOP code of the instruction.

Definition at line 954 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_nesting_closed()

void statement_list_typecheckt::typecheck_statement_list_nesting_closed ( const codet op_code)
private

Performs a typecheck on a Nesting Closed instruction.

Uses the latest entry on the nesting stack and modifies the RLO, OR and FC bit according to the instruction that started the nesting.

Parameters
op_codeOP code of the instruction.

Definition at line 962 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_networks()

void statement_list_typecheckt::typecheck_statement_list_networks ( const statement_list_parse_treet::tia_modulet tia_module,
symbolt tia_symbol 
)
private

Performs a typecheck on the networks of a TIA module and saves the result to the given symbol.

Parameters
tia_moduleModule containing the networks that shall be checked.
[out]tia_symbolSymbol representation of the given TIA module.

Definition at line 298 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_not()

void statement_list_typecheckt::typecheck_statement_list_not ( const codet op_code)
private

Performs a typecheck on a STL boolean NOT instruction.

Reads and modifies the RLO, OR and FC bit.

Parameters
op_codeOP code of the instruction.

Definition at line 758 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_or()

void statement_list_typecheckt::typecheck_statement_list_or ( const codet op_code,
const symbolt tia_element 
)
private

Performs a typecheck on a STL boolean Or instruction.

Reads and modifies the RLO, OR and FC bit.

Parameters
op_codeOP code of the instruction.
tia_elementSymbol representation of the TIA element.

Definition at line 816 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_or_not()

void statement_list_typecheckt::typecheck_statement_list_or_not ( const codet op_code,
const symbolt tia_element 
)
private

Performs a typecheck on a STL boolean Or Not instruction.

Reads and modifies the RLO, OR and FC bit.

Parameters
op_codeOP code of the instruction.
tia_elementSymbol representation of the TIA element.

Definition at line 841 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_reset()

void statement_list_typecheckt::typecheck_statement_list_reset ( const codet op_code,
symbolt tia_element 
)
private

Performs a typecheck on a STL 'R' instruction and saves the result to the given symbol.

Modifies the OR and FC bit.

Parameters
op_codeOP code of the instruction.
[out]tia_elementSymbol representation of the TIA element.

Definition at line 1077 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_set()

void statement_list_typecheckt::typecheck_statement_list_set ( const codet op_code,
symbolt tia_element 
)
private

Performs a typecheck on a STL 'S' instruction and saves the result to the given symbol.

Modifies the OR and FC bit.

Parameters
op_codeOP code of the instruction.
[out]tia_elementSymbol representation of the TIA element.

Definition at line 1060 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_set_rlo()

void statement_list_typecheckt::typecheck_statement_list_set_rlo ( const codet op_code)
private

Performs a typecheck on a STL 'SET' instruction and modifies the RLO, OR and FC bit.

Parameters
op_codeOP code of the instruction.

Definition at line 1042 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_transfer()

void statement_list_typecheckt::typecheck_statement_list_transfer ( const codet op_code,
symbolt tia_element 
)
private

Performs a typecheck on a STL transfer instruction and saves the result to the given symbol.

Modifies the accumulator.

Parameters
op_codeOP code of the instruction.
[out]tia_elementSymbol representation of the TIA element.

Definition at line 461 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_xor()

void statement_list_typecheckt::typecheck_statement_list_xor ( const codet op_code,
const symbolt tia_element 
)
private

Performs a typecheck on a STL boolean XOR instruction.

Reads and modifies the RLO, OR and FC bit.

Parameters
op_codeOP code of the instruction.
tia_elementSymbol representation of the TIA element.

Definition at line 862 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_xor_not()

void statement_list_typecheckt::typecheck_statement_list_xor_not ( const codet op_code,
const symbolt tia_element 
)
private

Performs a typecheck on a STL boolean XOR Not instruction.

Reads and modifies the RLO, OR and FC bit.

Parameters
op_codeOP code of the instruction.
tia_elementSymbol representation of the TIA element.

Definition at line 882 of file statement_list_typecheck.cpp.

◆ typecheck_tag_list()

void statement_list_typecheckt::typecheck_tag_list ( )
private

Performs a typecheck on the tag list of the referenced parse tree and adds symbols for its contents to the symbol table.

Definition at line 188 of file statement_list_typecheck.cpp.

◆ typecheck_temp_var_decls()

void statement_list_typecheckt::typecheck_temp_var_decls ( const statement_list_parse_treet::tia_modulet tia_module,
symbolt tia_symbol 
)
private

Performs a typecheck on the temp variables of a TIA module and saves the result to the given symbol value.

Parameters
tia_moduleElement whose temp declarations should be checked.
[out]tia_symbolSymbol representation of the TIA module.

Definition at line 276 of file statement_list_typecheck.cpp.

Member Data Documentation

◆ accumulator

std::vector<exprt> statement_list_typecheckt::accumulator
private

Representation of the accumulator of a TIA element.

Definition at line 73 of file statement_list_typecheck.h.

◆ fc_bit

bool statement_list_typecheckt::fc_bit = false
private

First Check (Part of the TIA status word).

Gets set every time a boolean instruction is encountered and is set to false once the boolean expression as a whole is terminated (either by an assignment or other instructions).

Definition at line 84 of file statement_list_typecheck.h.

◆ module

const irep_idt statement_list_typecheckt::module
private

Name of the module this typecheck belongs to.

Definition at line 66 of file statement_list_typecheck.h.

◆ nesting_stack

nesting_stackt statement_list_typecheckt::nesting_stack
private

Representation of the nesting stack.

Values are pushed once branching occurs and popped upon returning.

Definition at line 112 of file statement_list_typecheck.h.

◆ or_bit

bool statement_list_typecheckt::or_bit = false
private

Or (Part of the TIA status word).

Helps to track all And instructions that follow an operand-less Or instruction (The so called 'And before Or').

Definition at line 89 of file statement_list_typecheck.h.

◆ parse_tree

const statement_list_parse_treet& statement_list_typecheckt::parse_tree
private

Parse tree which is used to fill the symbol table.

Definition at line 60 of file statement_list_typecheck.h.

◆ rlo_bit

exprt statement_list_typecheckt::rlo_bit = true_exprt()
private

Result of Logic Operation (Part of the TIA status word).

Holds the current boolean expression of the active network and is read and modified by boolean instructions.

Definition at line 78 of file statement_list_typecheck.h.

◆ symbol_table

symbol_tablet& statement_list_typecheckt::symbol_table
private

Reference to the symbol table that should be filled during the typecheck.

Definition at line 63 of file statement_list_typecheck.h.


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