statement_list_typecheck.cpp File Reference

Statement List Language Type Checking. More...

#include "statement_list_typecheck.h"
#include <util/cprover_prefix.h>
#include <util/message.h>
#include <util/namespace.h>
#include <util/pointer_expr.h>
#include <util/simplify_expr.h>
#include <util/std_code.h>
#include <util/symbol_table_base.h>
#include <goto-programs/goto_instruction_code.h>
#include "converters/statement_list_types.h"

Include dependency graph for statement_list_typecheck.cpp:

Go to the source code of this file.

Macros
#define	STATEMENT_LIST_PTR_WIDTH   64
	Size of pointers in Siemens TIA. More...
#define	TYPECHECK_ERROR   0
#define	DATA_BLOCK_PARAMETER_NAME   "data_block"
	Artificial name for the data block interface of a function block. More...
#define	DATA_BLOCK_TYPE_POSTFIX   "_db"
	Postfix for the type of a data block. More...
#define	CPROVER_ASSERT   CPROVER_PREFIX "assert"
	Name of the CBMC assert function. More...
#define	CPROVER_ASSUME   CPROVER_PREFIX "assume"
	Name of the CBMC assume function. More...
#define	CPROVER_TEMP_RLO   CPROVER_PREFIX "temp_rlo"
	Name of the RLO symbol used in some operations. More...

Functions
static code_typet::parametert	create_data_block_parameter (const struct_typet &data_block_type, const irep_idt &function_block_name)
	Creates the artificial data block parameter with a generic name and the specified type. More...
bool	statement_list_typecheck (const statement_list_parse_treet &parse_tree, symbol_table_baset &symbol_table, const std::string &module, message_handlert &message_handler)
	Create a new statement_list_typecheckt object and perform a type check to fill the symbol table. More...

Variables
static const std::vector< irep_idt >	logic_sequence_initializers
static const std::vector< irep_idt >	logic_sequence_terminators

Detailed Description

Statement List Language Type Checking.

Definition in file statement_list_typecheck.cpp.

Macro Definition Documentation

CPROVER_ASSERT

#define CPROVER_ASSERT   CPROVER_PREFIX "assert"

Name of the CBMC assert function.

Definition at line 35 of file statement_list_typecheck.cpp.

CPROVER_ASSUME

#define CPROVER_ASSUME   CPROVER_PREFIX "assume"

Name of the CBMC assume function.

Definition at line 37 of file statement_list_typecheck.cpp.

CPROVER_TEMP_RLO

#define CPROVER_TEMP_RLO   CPROVER_PREFIX "temp_rlo"

Name of the RLO symbol used in some operations.

Definition at line 39 of file statement_list_typecheck.cpp.

DATA_BLOCK_PARAMETER_NAME

#define DATA_BLOCK_PARAMETER_NAME   "data_block"

Artificial name for the data block interface of a function block.

Definition at line 31 of file statement_list_typecheck.cpp.

DATA_BLOCK_TYPE_POSTFIX

#define DATA_BLOCK_TYPE_POSTFIX   "_db"

Postfix for the type of a data block.

Definition at line 33 of file statement_list_typecheck.cpp.

STATEMENT_LIST_PTR_WIDTH

#define STATEMENT_LIST_PTR_WIDTH   64

Size of pointers in Siemens TIA.

Definition at line 27 of file statement_list_typecheck.cpp.

TYPECHECK_ERROR

#define TYPECHECK_ERROR   0

Definition at line 29 of file statement_list_typecheck.cpp.

Function Documentation

create_data_block_parameter()

static code_typet::parametert create_data_block_parameter ( const struct_typet &  data_block_type, const irep_idt &  function_block_name  )

static

Creates the artificial data block parameter with a generic name and the specified type.

Parameters

data_block_type	Type of the data block.
function_block_name	Name of the function block to which this data block belongs.

Returns

Parameter of the data block.

Definition at line 70 of file statement_list_typecheck.cpp.

statement_list_typecheck()

bool statement_list_typecheck	(	const statement_list_parse_treet &	parse_tree,
		symbol_table_baset &	symbol_table,
		const std::string &	module,
		message_handlert &	message_handler
	)

Create a new statement_list_typecheckt object and perform a type check to fill the symbol table.

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.

Returns

False if no errors occurred, true otherwise.

Definition at line 82 of file statement_list_typecheck.cpp.

Variable Documentation

logic_sequence_initializers

const std::vector<irep_idt> logic_sequence_initializers

static

Initial value:

= {
  ID_statement_list_and,
  ID_statement_list_and_not,
  ID_statement_list_or,
  ID_statement_list_or_not,
  ID_statement_list_xor,
  ID_statement_list_xor_not,
  ID_statement_list_and_nested,
  ID_statement_list_and_not_nested,
  ID_statement_list_or_nested,
  ID_statement_list_or_not_nested,
  ID_statement_list_xor_nested,
  ID_statement_list_xor_not_nested,
}

Definition at line 41 of file statement_list_typecheck.cpp.

logic_sequence_terminators

const std::vector<irep_idt> logic_sequence_terminators

static

Initial value:

= {
  ID_statement_list_set_rlo,
  ID_statement_list_clr_rlo,
  ID_statement_list_set,
  ID_statement_list_reset,
  ID_statement_list_assign,
}

Definition at line 56 of file statement_list_typecheck.cpp.