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

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

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

Public Member Functions
	statement_list_typecheckt (const statement_list_parse_treet &parse_tree, symbol_table_baset &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_handlert &	get_message_handler ()

	messaget ()

	messaget (const messaget &other)

messaget &	operator= (const messaget &other)

	messaget (message_handlert &_message_handler)

virtual	~messaget ()

mstreamt &	get_mstream (unsigned message_level) const

mstreamt &	error () const

mstreamt &	warning () const

mstreamt &	result () const

mstreamt &	status () const

mstreamt &	statistics () const

mstreamt &	progress () const

mstreamt &	debug () 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 >

using	stl_labelst = std::unordered_map< irep_idt, stl_label_locationt >

using	label_referencest = std::unordered_map< irep_idt, std::vector< stl_jump_locationt > >

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_label_references ()
	Checks if all jumps reference labels that exist. 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_code (const codet &instruction, symbolt &tia_element)
	Performs a typecheck for the specified instruction in code form. More...

void	typecheck_label (const codet &instruction, symbolt &tia_element)
	Performs a typecheck for the given label in code form. 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_jump_unconditional (const codet &op_code, symbolt &tia_element)
	Performs a typecheck on an unconditional jump instruction (JU) and adds the jump to the given symbol. More...

void	typecheck_statement_list_jump_conditional (const codet &op_code, symbolt &tia_element)
	Performs a typecheck on a conditional jump instruction (JC) and adds it to the given symbol. More...

void	typecheck_statement_list_jump_conditional_not (const codet &op_code, symbolt &tia_element)
	Performs a typecheck on a inverted conditional jump instruction (JCN) and adds it to the given symbol. More...

stl_label_locationt	typecheck_label_location (const code_labelt &label)
	Converts the properties of the current typecheck state to a label location. More...

void	typecheck_jump_locations (const code_labelt &label, const stl_label_locationt &location)
	Performs a typecheck on all references for the given label. 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_exprt &	typecheck_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...

void	typecheck_label_reference (const irep_idt &label, bool sets_fc_false)
	Checks if the given label is already present and compares the current state with it. 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< code_frontend_assignt > &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< code_frontend_assignt > &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	clear_module_state ()
	Modifies the state of the typecheck to resemble the beginning of a new module. More...

void	clear_network_state ()
	Modifies the state of the typecheck to resemble the beginning of a new network. 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_treet &	parse_tree
	Parse tree which is used to fill the symbol table. More...

symbol_table_baset &	symbol_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< exprt >	accumulator
	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...

stl_labelst	stl_labels
	Data structure that contains data about the labels of the current module. More...

label_referencest	label_references
	Holds associations between labels and jumps that are referencing it. 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_handlert *	message_handler

mstreamt	mstream

Detailed Description

Class for encapsulating the current state of the type check.

Definition at line 42 of file statement_list_typecheck.h.

Member Typedef Documentation

◆ label_referencest

using statement_list_typecheckt::label_referencest = std::unordered_map<irep_idt, std::vector<stl_jump_locationt> >

private

Definition at line 170 of file statement_list_typecheck.h.

◆ nesting_stackt

using statement_list_typecheckt::nesting_stackt = std::vector<nesting_stack_entryt>

private

Definition at line 113 of file statement_list_typecheck.h.

◆ stl_labelst

using statement_list_typecheckt::stl_labelst = std::unordered_map<irep_idt, stl_label_locationt>

private

Definition at line 146 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_table_baset &	symbol_table,
		const std::string &	module,
		message_handlert &	message_handler
	)

Creates a new instance of statement_list_typecheckt.

Parameters

	parse_tree	Parse tree generated by parsing a Statement List file.
[out]	symbol_table	Object 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.
	module	Name of the file that has been parsed.
	message_handler	Used to provide debug information and error messages.

Definition at line 118 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 238 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

op	Operand to be added to the Or instruction.

Definition at line 1773 of file statement_list_typecheck.cpp.

◆ clear_module_state()

void statement_list_typecheckt::clear_module_state ( )

private

Modifies the state of the typecheck to resemble the beginning of a new module.

All changes to the implicit typecheck fields are close to the original TIA behaviour.

Definition at line 1808 of file statement_list_typecheck.cpp.

◆ clear_network_state()

void statement_list_typecheckt::clear_network_state ( )

private

Modifies the state of the typecheck to resemble the beginning of a new network.

All changes to the implicit typecheck fields are close to the original TIA behaviour.

Definition at line 1800 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_block Function 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 248 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

op	Operand of the encountered instruction.

Definition at line 1793 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_element Symbol representation of the TIA element.

Definition at line 1815 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 130 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

comparison ID of the compare expression that should be pushed to the RLO.

Definition at line 1403 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_code OP code of the instruction.

Definition at line 1482 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_code	OP code of the instruction.
[out]	tia_element	Symbol representation of the TIA element.

Definition at line 1643 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_code	OP code of the instruction.
[out]	tia_element	Symbol representation of the TIA element.

Definition at line 1687 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_code	OP code of the instruction.
[out]	tia_element	Symbol representation of the TIA element.

Definition at line 1621 of file statement_list_typecheck.cpp.

◆ typecheck_code()

void statement_list_typecheckt::typecheck_code	(	const codet &	instruction,
		symbolt &	tia_element
	)

private

Performs a typecheck for the specified instruction in code form.

Parameters

	instruction	Code to check.
[out]	tia_element	Symbol representation of the TIA module.

Definition at line 374 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_code	OP code of the instruction.
[out]	tia_element	Symbol representation of the TIA element.

Definition at line 1583 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_code	OP code of the instruction.
[out]	tia_element	Symbol representation of the TIA element.

Definition at line 1602 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_block Function block to be checked.

Definition at line 157 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_decls	List of declarations which should be typechecked.
[out]	components	List of typechecked and converted declarations.
	var_property	Type of variable declaration list (for example input, output, ...).

Definition at line 264 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_element	Symbol representation of the TIA element.
rhs	Expression that the function parameter got assigned to.

Returns: Expression of either a symbol or a constant.

Definition at line 1730 of file statement_list_typecheck.cpp.

◆ typecheck_function_call_arguments()

exprt statement_list_typecheckt::typecheck_function_call_arguments	(	const std::vector< code_frontend_assignt > &	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

assignments	Assignment list of the function call.
param	Parameter that should be checked.
tia_element	Symbol representation of the TIA element.

Returns: Expression including the assigned symbol's name and type.

Definition at line 1699 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

function Function to be checked.

Definition at line 204 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_decls	List of declarations which should be typechecked.
[out]	params	List of typechecked and converted declarations.
	function_name	Function to which the variable list belongs (used for naming).
	var_property	Type of variable declaration list (for example input, output, ...).

Definition at line 280 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

identifier	Identifier that should be checked.
tia_element	Symbol representation of the current TIA module.

Returns: Expression including the symbol's name and type.

Definition at line 1521 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_code OP code of the instruction.

Returns: Reference to the operand.

Definition at line 1459 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_code OP code of the instruction.

Definition at line 1472 of file statement_list_typecheck.cpp.

◆ typecheck_jump_locations()

void statement_list_typecheckt::typecheck_jump_locations	(	const code_labelt &	label,
		const stl_label_locationt &	location
	)

private

Performs a typecheck on all references for the given label.

Parameters

label	Label to check.
location	Data about the location of the label.

Definition at line 589 of file statement_list_typecheck.cpp.

◆ typecheck_label()

void statement_list_typecheckt::typecheck_label	(	const codet &	instruction,
		symbolt &	tia_element
	)

private

Performs a typecheck for the given label in code form.

Parameters

	instruction	Label to check.
[out]	tia_element	Symbol representation of the TIA module.

Definition at line 502 of file statement_list_typecheck.cpp.

◆ typecheck_label_location()

statement_list_typecheckt::stl_label_locationt statement_list_typecheckt::typecheck_label_location ( const code_labelt & label )

private

Converts the properties of the current typecheck state to a label location.

Parameters

label Label to check the properties for.

Returns: Encoded location information for the given label.

Definition at line 540 of file statement_list_typecheck.cpp.

◆ typecheck_label_reference()

void statement_list_typecheckt::typecheck_label_reference	(	const irep_idt &	label,
		bool	sets_fc_false
	)

private

Checks if the given label is already present and compares the current state with it.

If there is no entry for the label, a new jump location is added to the typecheck for later verification.

Parameters

label	Label to check.
sets_fc_false	Whether the encountered jump instruction sets the /FC bit to false.

Definition at line 1413 of file statement_list_typecheck.cpp.

◆ typecheck_label_references()

void statement_list_typecheckt::typecheck_label_references ( )

private

Checks if all jumps reference labels that exist.

Definition at line 351 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_code	OP code of the instruction.
rlo_value	Value 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 1493 of file statement_list_typecheck.cpp.

◆ typecheck_return_value_assignment()

exprt statement_list_typecheckt::typecheck_return_value_assignment	(	const std::vector< code_frontend_assignt > &	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

assignments	Assignment list of the function call.
return_type	Type of the return value.
tia_element	Symbol representation of the TIA element.

Returns: Expression including the assigned symbol's name and type.

Definition at line 1745 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_code	OP code of the instruction.
tia_element	Symbol representation of the TIA element.
negate	Whether the operand should be negated (e.g. for the `AND NOT` expression).

Returns: Typechecked operand.

Definition at line 1509 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_code OP code of the instruction.

Definition at line 756 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_code OP code of the instruction.

Definition at line 1365 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_code OP code of the instruction.

Definition at line 795 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_code OP code of the instruction.

Definition at line 808 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_code OP code of the instruction.

Definition at line 829 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_code OP code of the instruction.

Definition at line 843 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_code OP code of the instruction.

Definition at line 822 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_code OP code of the instruction.

Definition at line 836 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_code OP code of the instruction.

Definition at line 782 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_code OP code of the instruction.

Definition at line 815 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_code OP code of the instruction.

Definition at line 769 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_code OP code of the instruction.

Definition at line 662 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_code OP code of the instruction.

Definition at line 1344 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_code OP code of the instruction.

Definition at line 701 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_code OP code of the instruction.

Definition at line 714 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_code OP code of the instruction.

Definition at line 735 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_code OP code of the instruction.

Definition at line 749 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_code OP code of the instruction.

Definition at line 728 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_code OP code of the instruction.

Definition at line 742 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_code OP code of the instruction.

Definition at line 688 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_code OP code of the instruction.

Definition at line 721 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_code OP code of the instruction.

Definition at line 675 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_code OP code of the instruction.

Definition at line 850 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_code OP code of the instruction.

Definition at line 1387 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_code OP code of the instruction.

Definition at line 889 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_code OP code of the instruction.

Definition at line 902 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_code OP code of the instruction.

Definition at line 923 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_code OP code of the instruction.

Definition at line 937 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_code OP code of the instruction.

Definition at line 916 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_code OP code of the instruction.

Definition at line 930 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_code OP code of the instruction.

Definition at line 876 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_code OP code of the instruction.

Definition at line 909 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_code OP code of the instruction.

Definition at line 863 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_code	OP code of the instruction.
tia_element	Symbol representation of the TIA element.

Definition at line 952 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 1083 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_code	OP code of the instruction.
tia_element	Symbol representation of the TIA element.

Definition at line 974 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_code	OP code of the instruction.
[out]	tia_element	Symbol representation of the TIA element.

Definition at line 1201 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_code	OP code of the instruction.
[out]	tia_element	Symbol representation of the TIA element.

Definition at line 1274 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_code OP code of the instruction.

Definition at line 1231 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

	instruction	Instruction that should be checked.
[out]	tia_element	Symbol representation of the TIA module.

Definition at line 366 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_jump_conditional()

void statement_list_typecheckt::typecheck_statement_list_jump_conditional	(	const codet &	op_code,
		symbolt &	tia_element
	)

private

Performs a typecheck on a conditional jump instruction (JC) and adds it to the given symbol.

Modifies the /FC, RLO and OR bits.

Parameters

	op_code	OP code of the instruction.
[out]	tia_element	Symbol representation of the TIA element.

Definition at line 1308 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_jump_conditional_not()

void statement_list_typecheckt::typecheck_statement_list_jump_conditional_not	(	const codet &	op_code,
		symbolt &	tia_element
	)

private

Performs a typecheck on a inverted conditional jump instruction (JCN) and adds it to the given symbol.

Modifies the /FC, RLO and OR bits.

Parameters

	op_code	OP code of the instruction.
[out]	tia_element	Symbol representation of the TIA element.

Definition at line 1326 of file statement_list_typecheck.cpp.

◆ typecheck_statement_list_jump_unconditional()

void statement_list_typecheckt::typecheck_statement_list_jump_unconditional	(	const codet &	op_code,
		symbolt &	tia_element
	)

private

Performs a typecheck on an unconditional jump instruction (JU) and adds the jump to the given symbol.

Parameters

	op_code	OP code of the instruction.
[out]	tia_element	Symbol representation of the TIA element.

Definition at line 1295 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_code	OP code of the instruction.
tia_element	Symbol representation of the TIA element.

Definition at line 626 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_code OP code of the instruction.

Definition at line 1094 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_code OP code of the instruction.

Definition at line 1102 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_code OP code of the instruction.

Definition at line 1110 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_code OP code of the instruction.

Definition at line 1118 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_code OP code of the instruction.

Definition at line 1126 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_code OP code of the instruction.

Definition at line 1134 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_code OP code of the instruction.

Definition at line 1142 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_module	Module containing the networks that shall be checked.
[out]	tia_symbol	Symbol representation of the given TIA module.

Definition at line 329 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_code OP code of the instruction.

Definition at line 944 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_code	OP code of the instruction.
tia_element	Symbol representation of the TIA element.

Definition at line 996 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_code	OP code of the instruction.
tia_element	Symbol representation of the TIA element.

Definition at line 1021 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_code	OP code of the instruction.
[out]	tia_element	Symbol representation of the TIA element.

Definition at line 1257 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_code	OP code of the instruction.
[out]	tia_element	Symbol representation of the TIA element.

Definition at line 1240 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_code OP code of the instruction.

Definition at line 1222 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_code	OP code of the instruction.
[out]	tia_element	Symbol representation of the TIA element.

Definition at line 647 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_code	OP code of the instruction.
tia_element	Symbol representation of the TIA element.

Definition at line 1042 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_code	OP code of the instruction.
tia_element	Symbol representation of the TIA element.

Definition at line 1062 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 225 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_module	Element whose temp declarations should be checked.
[out]	tia_symbol	Symbol representation of the TIA module.

Definition at line 307 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 78 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 89 of file statement_list_typecheck.h.

◆ label_references

label_referencest statement_list_typecheckt::label_references

private

Holds associations between labels and jumps that are referencing it.

This list should be empty after a successful typecheck. A new entry is added only if a jump is encountered that references an unknown label. It is removed once the label is encountered and the jump is valid.

Definition at line 177 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 71 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 117 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 94 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 65 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 83 of file statement_list_typecheck.h.

◆ stl_labels

stl_labelst statement_list_typecheckt::stl_labels

private

Data structure that contains data about the labels of the current module.

Definition at line 149 of file statement_list_typecheck.h.

◆ symbol_table

symbol_table_baset& statement_list_typecheckt::symbol_table

private

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

Definition at line 68 of file statement_list_typecheck.h.

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

/home/runner/work/cbmc/cbmc/src/statement-list/statement_list_typecheck.h
/home/runner/work/cbmc/cbmc/src/statement-list/statement_list_typecheck.cpp

Classes

Public Member Functions

Private Types

Private Member Functions

Private Attributes

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ label_referencest

◆ nesting_stackt

◆ stl_labelst

Constructor & Destructor Documentation

◆ statement_list_typecheckt()

Member Function Documentation

◆ add_temp_rlo()

◆ add_to_or_rlo_wrapper()

◆ clear_module_state()

◆ clear_network_state()

◆ create_instance_data_block_type()

◆ initialize_bit_expression()

◆ save_rlo_state()

◆ typecheck()

◆ typecheck_accumulator_compare_instruction()

◆ typecheck_binary_accumulator_instruction()

◆ typecheck_called_function()

◆ typecheck_called_function_block()

◆ typecheck_called_tia_element()

◆ typecheck_code()

◆ typecheck_CPROVER_assert()

◆ typecheck_CPROVER_assume()

◆ typecheck_function_block_declaration()

◆ typecheck_function_block_var_decls()

◆ typecheck_function_call_argument_rhs()

◆ typecheck_function_call_arguments()

◆ typecheck_function_declaration()

◆ typecheck_function_var_decls()

◆ typecheck_identifier()

◆ typecheck_instruction_with_non_const_operand()

◆ typecheck_instruction_without_operand()

◆ typecheck_jump_locations()

◆ typecheck_label()

◆ typecheck_label_location()

◆ typecheck_label_reference()

◆ typecheck_label_references()

◆ typecheck_nested_boolean_instruction()

◆ typecheck_return_value_assignment()

◆ typecheck_simple_boolean_instruction_operand()

◆ typecheck_statement_list_accu_dint_add()

◆ typecheck_statement_list_accu_dint_arith()

◆ typecheck_statement_list_accu_dint_div()

◆ typecheck_statement_list_accu_dint_eq()

◆ typecheck_statement_list_accu_dint_gt()

◆ typecheck_statement_list_accu_dint_gte()

◆ typecheck_statement_list_accu_dint_lt()

◆ typecheck_statement_list_accu_dint_lte()

◆ typecheck_statement_list_accu_dint_mul()

◆ typecheck_statement_list_accu_dint_neq()

◆ typecheck_statement_list_accu_dint_sub()

◆ typecheck_statement_list_accu_int_add()

◆ typecheck_statement_list_accu_int_arith()

◆ typecheck_statement_list_accu_int_div()

◆ typecheck_statement_list_accu_int_eq()

◆ typecheck_statement_list_accu_int_gt()

◆ typecheck_statement_list_accu_int_gte()

◆ typecheck_statement_list_accu_int_lt()

◆ typecheck_statement_list_accu_int_lte()

◆ typecheck_statement_list_accu_int_mul()

◆ typecheck_statement_list_accu_int_neq()

◆ typecheck_statement_list_accu_int_sub()

◆ typecheck_statement_list_accu_real_add()

◆ typecheck_statement_list_accu_real_arith()

◆ typecheck_statement_list_accu_real_div()

◆ typecheck_statement_list_accu_real_eq()

◆ typecheck_statement_list_accu_real_gt()

◆ typecheck_statement_list_accu_real_gte()

◆ typecheck_statement_list_accu_real_lt()

◆ typecheck_statement_list_accu_real_lte()

◆ typecheck_statement_list_accu_real_mul()

◆ typecheck_statement_list_accu_real_neq()

◆ typecheck_statement_list_accu_real_sub()