Go to the documentation of this file.
25 #define STATEMENT_LIST_PTR_WIDTH 64
27 #define TYPECHECK_ERROR 0
28 #define DATA_BLOCK_PARAMETER_NAME "data_block"
30 #define DATA_BLOCK_TYPE_POSTFIX "_db"
32 #define CPROVER_ASSERT CPROVER_PREFIX "assert"
34 #define CPROVER_ASSUME CPROVER_PREFIX "assume"
36 #define CPROVER_TEMP_RLO CPROVER_PREFIX "temp_rlo"
60 const std::string &module,
64 parse_tree, symbol_table, module, message_handler);
73 : rlo_bit(rlo_bit), or_bit(or_bit), function_code(function_code)
122 function_block_sym.
name = function_block.
name;
125 function_block_sym.
mode = ID_statement_list;
140 data_block.base_name = data_block.name;
141 data_block.mode = ID_statement_list;
149 param_sym.
type = param.type();
150 param_sym.
name = param.get_identifier();
153 param_sym.
mode = ID_statement_list;
158 params.push_back(param);
160 fb_type.
set(ID_statement_list_type, ID_statement_list_function_block);
161 function_block_sym.
type = fb_type;
170 function_sym.
name =
function.name;
173 function_sym.
mode = ID_statement_list;
176 function.var_input, params,
function.name, ID_statement_list_var_input);
178 function.var_inout, params,
function.name, ID_statement_list_var_inout);
180 function.var_output, params,
function.name, ID_statement_list_var_output);
183 fc_type.
set(ID_statement_list_type, ID_statement_list_function);
184 function_sym.
type = fc_type;
199 tag_sym.
mode = ID_statement_list;
213 temp_rlo.
mode = ID_statement_list;
222 function_block.
var_input, components, ID_statement_list_var_input);
224 function_block.
var_inout, components, ID_statement_list_var_inout);
226 function_block.
var_output, components, ID_statement_list_var_output);
228 function_block.
var_static, components, ID_statement_list_var_static);
241 const irep_idt &var_name{declaration.variable.get_identifier()};
242 const typet &var_type{declaration.variable.type()};
244 component.set(ID_statement_list_type, var_property);
260 param_sym.
type = declaration.variable.type();
262 "::" +
id2string(declaration.variable.get_identifier());
263 param_sym.
base_name = declaration.variable.get_identifier();
265 param_sym.
mode = ID_statement_list;
269 param.set_identifier(param_sym.
name);
270 param.set_base_name(declaration.variable.get_identifier());
271 param.
set(ID_statement_list_type, var_property);
272 params.push_back(param);
289 temp_sym.
mode = ID_statement_list;
310 for(
const auto &network : tia_module.
networks)
314 for(
const auto &instruction : network.instructions)
324 const irep_idt statement{op_code.get_statement()};
326 if(ID_statement_list_load == statement)
328 else if(ID_statement_list_transfer == statement)
330 else if(ID_statement_list_accu_int_add == statement)
332 else if(ID_statement_list_accu_int_sub == statement)
334 else if(ID_statement_list_accu_int_mul == statement)
336 else if(ID_statement_list_accu_int_div == statement)
338 else if(ID_statement_list_accu_int_eq == statement)
340 else if(ID_statement_list_accu_int_neq == statement)
342 else if(ID_statement_list_accu_int_lt == statement)
344 else if(ID_statement_list_accu_int_gt == statement)
346 else if(ID_statement_list_accu_int_lte == statement)
348 else if(ID_statement_list_accu_int_gte == statement)
350 else if(ID_statement_list_accu_dint_add == statement)
352 else if(ID_statement_list_accu_dint_sub == statement)
354 else if(ID_statement_list_accu_dint_mul == statement)
356 else if(ID_statement_list_accu_dint_div == statement)
358 else if(ID_statement_list_accu_dint_eq == statement)
360 else if(ID_statement_list_accu_dint_neq == statement)
362 else if(ID_statement_list_accu_dint_lt == statement)
364 else if(ID_statement_list_accu_dint_gt == statement)
366 else if(ID_statement_list_accu_dint_lte == statement)
368 else if(ID_statement_list_accu_dint_gte == statement)
370 else if(ID_statement_list_accu_real_add == statement)
372 else if(ID_statement_list_accu_real_sub == statement)
374 else if(ID_statement_list_accu_real_mul == statement)
376 else if(ID_statement_list_accu_real_div == statement)
378 else if(ID_statement_list_accu_real_eq == statement)
380 else if(ID_statement_list_accu_real_neq == statement)
382 else if(ID_statement_list_accu_real_lt == statement)
384 else if(ID_statement_list_accu_real_gt == statement)
386 else if(ID_statement_list_accu_real_lte == statement)
388 else if(ID_statement_list_accu_real_gte == statement)
390 else if(ID_statement_list_not == statement)
392 else if(ID_statement_list_and == statement)
394 else if(ID_statement_list_and_not == statement)
396 else if(ID_statement_list_or == statement)
398 else if(ID_statement_list_or_not == statement)
400 else if(ID_statement_list_xor == statement)
402 else if(ID_statement_list_xor_not == statement)
404 else if(ID_statement_list_and_nested == statement)
406 else if(ID_statement_list_and_not_nested == statement)
408 else if(ID_statement_list_or_nested == statement)
410 else if(ID_statement_list_or_not_nested == statement)
412 else if(ID_statement_list_xor_nested == statement)
414 else if(ID_statement_list_xor_not_nested == statement)
416 else if(ID_statement_list_nesting_closed == statement)
418 else if(ID_statement_list_assign == statement)
420 else if(ID_statement_list_set_rlo == statement)
422 else if(ID_statement_list_clr_rlo == statement)
424 else if(ID_statement_list_set == statement)
426 else if(ID_statement_list_reset == statement)
428 else if(ID_statement_list_nop == statement)
430 else if(ID_statement_list_call == statement)
434 error() <<
"OP code of instruction not found: " << op_code.get_statement()
441 const codet &op_code,
445 expr_try_dynamic_cast<symbol_exprt>(op_code.
op0());
456 error() <<
"Instruction is not followed by symbol or constant" <<
eom;
462 const codet &op_code,
469 error() <<
"Types of transfer assignment do not match" <<
eom;
477 const codet &op_code)
490 const codet &op_code)
503 const codet &op_code)
516 const codet &op_code)
529 const codet &op_code)
536 const codet &op_code)
543 const codet &op_code)
550 const codet &op_code)
557 const codet &op_code)
564 const codet &op_code)
571 const codet &op_code)
584 const codet &op_code)
597 const codet &op_code)
610 const codet &op_code)
623 const codet &op_code)
630 const codet &op_code)
637 const codet &op_code)
644 const codet &op_code)
651 const codet &op_code)
658 const codet &op_code)
665 const codet &op_code)
678 const codet &op_code)
691 const codet &op_code)
704 const codet &op_code)
717 const codet &op_code)
724 const codet &op_code)
731 const codet &op_code)
738 const codet &op_code)
745 const codet &op_code)
752 const codet &op_code)
759 const codet &op_code)
773 const codet &op_code,
795 const codet &op_code,
817 const codet &op_code,
842 const codet &op_code,
863 const codet &op_code,
883 const codet &op_code,
915 const codet &op_code)
923 const codet &op_code)
931 const codet &op_code)
939 const codet &op_code)
947 const codet &op_code)
955 const codet &op_code)
963 const codet &op_code)
968 error() <<
"Wrong order of brackets (Right parenthesis is not preceded by "
976 if(ID_statement_list_and_nested == statement)
987 else if(ID_statement_list_and_not_nested == statement)
998 else if(ID_statement_list_or_nested == statement)
1003 else if(ID_statement_list_or_not_nested == statement)
1008 else if(ID_statement_list_xor_nested == statement)
1013 else if(ID_statement_list_xor_not_nested == statement)
1022 const codet &op_code,
1030 error() <<
"Types of assign do not match" <<
eom;
1043 const codet &op_code)
1052 const codet &op_code)
1061 const codet &op_code,
1065 const irep_idt &identifier{op.get_identifier()};
1078 const codet &op_code,
1082 const irep_idt &identifier{op.get_identifier()};
1095 const codet &op_code,
1099 const irep_idt &identifier{op.get_identifier()};
1108 error() <<
"Called function could not be found" <<
eom;
1116 const codet &op_code)
1124 type_try_dynamic_cast<signedbv_typet>(accu1.type());
1126 type_try_dynamic_cast<signedbv_typet>(accu2.type());
1131 error() <<
"Operands of integer addition are no integers" <<
eom;
1137 const codet &op_code)
1145 type_try_dynamic_cast<signedbv_typet>(accu1.type());
1147 type_try_dynamic_cast<signedbv_typet>(accu2.type());
1152 error() <<
"Operands of double integer addition are no double integers"
1159 const codet &op_code)
1169 error() <<
"Operands of Real addition do not have the type Real" <<
eom;
1186 const codet &op_code)
1189 expr_try_dynamic_cast<symbol_exprt>(op_code.
op0());
1194 error() <<
"Instruction is not followed by symbol" <<
eom;
1199 const codet &op_code)
1203 error() <<
"Instruction is followed by operand" <<
eom;
1209 const codet &op_code)
1214 error() <<
"Not enough operands in the accumulator" <<
eom;
1220 const codet &op_code,
1221 const exprt &rlo_value)
1236 const codet &op_code,
1244 return negate ? not_op : op;
1267 element_type.get(ID_statement_list_type) ==
1268 ID_statement_list_function_block)
1275 type_try_dynamic_cast<struct_typet>(db_expr.
type().
subtype());
1280 if(member.get_name() == identifier)
1289 element_type.get(ID_statement_list_type) == ID_statement_list_function)
1292 for(
const auto &member : element_type.parameters())
1294 if(member.get_base_name() == identifier)
1305 error() <<
"Identifier could not be found in project" <<
eom;
1310 const codet &op_code,
1314 expr_try_dynamic_cast<equal_exprt>(op_code.
op1());
1323 error() <<
"No assignment found for assertion" <<
eom;
1329 const codet &op_code,
1333 expr_try_dynamic_cast<equal_exprt>(op_code.
op1());
1342 error() <<
"No assignment found for assumption" <<
eom;
1348 const codet &op_code,
1352 const symbolt &called_function{
1357 called_type.get(ID_statement_list_type) == ID_statement_list_function_block)
1359 else if(called_type.get(ID_statement_list_type) == ID_statement_list_function)
1363 error() <<
"Tried to call element that is no function or function block"
1370 const codet &op_code,
1374 const symbolt &called_function_sym{
1376 const symbol_exprt called_function_expr{called_function_sym.symbol_expr()};
1382 error() <<
"Function calls should not address instance data blocks" <<
eom;
1389 std::vector<equal_exprt> assignments;
1390 for(
const auto &expr : op_code.
operands())
1401 if(called_type.return_type().is_nil())
1407 assignments, called_type.return_type(), tia_element)};
1414 const codet &op_code,
1421 error() <<
"Calls to function blocks are not supported yet" <<
eom;
1426 const std::vector<equal_exprt> &assignments,
1435 if(param_name == lhs.get_identifier())
1437 exprt assigned_variable{
1440 if(param_type == assigned_variable.type())
1441 return assigned_variable;
1444 error() <<
"Types of parameter assignment do not match: "
1445 << param.
type().
id() <<
" != " << assigned_variable.type().id()
1451 error() <<
"No assignment found for function parameter "
1460 exprt assigned_operand;
1462 expr_try_dynamic_cast<symbol_exprt>(rhs);
1467 assigned_operand = rhs;
1468 return assigned_operand;
1472 const std::vector<equal_exprt> &assignments,
1473 const typet &return_type,
1479 if(ID_statement_list_return_value_id == lhs.get_identifier())
1482 const exprt assigned_variable{
1484 if(return_type == assigned_variable.type())
1485 return assigned_variable;
1488 error() <<
"Types of return value assignment do not match: "
1489 << return_type.
id() <<
" != " << assigned_variable.type().id()
1495 error() <<
"No assignment found for function return value" <<
eom;
1509 or_wrapper.op1() = and_op;
1514 or_wrapper.
op1() = and_op;
1532 rlo_bit = std::move(temp_rlo);
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.
void typecheck_statement_list_nested_and_not(const codet &op_code)
Performs a typecheck on a nested And Not instruction.
#define UNREACHABLE
This should be used to mark dead code.
const componentst & components() const
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
A codet representing sequential composition of program statements.
void typecheck_statement_list_and_not(const codet &op_code, const symbolt &tia_element)
Performs a typecheck on a STL boolean And Not instruction.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
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.
const typet & subtype() const
void typecheck_statement_list_and_before_or()
Performs a typecheck on a STL operand-less Or instruction.
void typecheck_statement_list_accu_int_arith(const codet &op_code)
Performs a typecheck on a STL Accumulator instruction for integers.
void typecheck_statement_list_accu_int_gt(const codet &op_code)
Performs a typecheck on a STL accumulator greater than comparison instruction for integers.
Statement List Language Type Checking.
networkst networks
List of all networks of this module.
void typecheck_statement_list_not(const codet &op_code)
Performs a typecheck on a STL boolean NOT instruction.
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.
const irep_idt module
Name of the module this typecheck belongs to.
void typecheck_statement_list_nested_or_not(const codet &op_code)
Performs a typecheck on a nested Or Not instruction.
std::list< var_declarationt > var_declarationst
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.
The type of an expression, extends irept.
std::vector< parametert > parameterst
var_declarationst var_temp
Temp variable declarations.
typet type
Type of symbol.
Operator to dereference a pointer.
void typecheck_statement_list_accu_real_eq(const codet &op_code)
Performs a typecheck on a STL accumulator equality comparison instruction for double integers.
void set_identifier(const irep_idt &identifier)
void typecheck_statement_list_accu_real_sub(const codet &op_code)
Performs a typecheck on a STL accumulator subtract instruction for reals.
void typecheck_statement_list_nested_and(const codet &op_code)
Performs a typecheck on a nested And instruction.
void typecheck_statement_list_accu_dint_sub(const codet &op_code)
Performs a typecheck on a STL accumulator subtract instruction for double integers.
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.
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.
A codet representing the declaration of a local variable.
A non-fatal assertion, which checks a condition then permits execution to continue.
Struct for a single variable declaration in Statement List.
The plus expression Associativity is not specified.
var_declarationst var_input
Input variable declarations.
void typecheck_statement_list_accu_real_add(const codet &op_code)
Performs a typecheck on a STL accumulator add instruction for reals.
#define CPROVER_TEMP_RLO
Name of the RLO symbol used in some operations.
Base class for all expressions.
std::vector< componentt > componentst
irep_idt base_name
Base (non-scoped) name.
symbol_tablet & symbol_table
Reference to the symbol table that should be filled during the typecheck.
Represents a regular Statement List instruction which consists out of one or more codet tokens.
Base element of all modules in the Totally Integrated Automation (TIA) portal by Siemens.
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
void typecheck_statement_list_accu_dint_arith(const codet &op_code)
Performs a typecheck on a STL Accumulator instruction for double integers.
void save_rlo_state(symbolt &tia_element)
Saves the current RLO bit to a temporary variable to prevent false overrides when modifying boolean v...
symbol_exprt variable
Representation of the variable, including identifier and type.
exprt rlo_bit
Result of Logic Operation (Part of the TIA status word).
void typecheck_statement_list_accu_int_neq(const codet &op_code)
Performs a typecheck on a STL accumulator inequality comparison instruction for integers.
Expression to hold a symbol (variable)
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 necessa...
void typecheck_statement_list_accu_int_add(const codet &op_code)
Performs a typecheck on a STL accumulator add instruction for integers.
#define CPROVER_ASSUME
Name of the CBMC assume function.
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 v...
void typecheck_statement_list_accu_real_div(const codet &op_code)
Performs a typecheck on a STL accumulator divide instruction for reals.
nesting_stack_entryt(exprt rlo_bit, bool or_bit, codet function_code)
void typecheck_tag_list()
Performs a typecheck on the tag list of the referenced parse tree and adds symbols for its contents t...
Structure for a simple function block in Statement List.
bool can_cast_expr< equal_exprt >(const exprt &base)
codet representation of an if-then-else statement.
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 intege...
irep_idt pretty_name
Language-specific display name.
void typecheck_statement_list_nested_xor_not(const codet &op_code)
Performs a typecheck on a nested XOR Not instruction.
void typecheck_statement_list_or(const codet &op_code, const symbolt &tia_element)
Performs a typecheck on a STL boolean Or instruction.
void typecheck_statement_list_accu_int_sub(const codet &op_code)
Performs a typecheck on a STL accumulator subtract instruction for integers.
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.
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.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
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.
typet & type()
Return the type of the expression.
exprt typecheck_function_call_arguments(const std::vector< equal_exprt > &assignments, const code_typet::parametert ¶m, const symbolt &tia_element)
Checks if the given parameter is inside of the assignment list of a function call and returns the exp...
codet representation of a function call statement.
bool can_cast_expr< and_exprt >(const exprt &base)
void typecheck_statement_list_accu_dint_eq(const codet &op_code)
Performs a typecheck on a STL accumulator equality comparison instruction for double integers.
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.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
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.
nesting_stackt nesting_stack
Representation of the nesting stack.
irep_idt mode
Language mode.
const irep_idt & get_base_name() const
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.
void typecheck_statement_list_load(const codet &op_code, const symbolt &tia_element)
Performs a typecheck on a STL load instruction.
void typecheck_binary_accumulator_instruction(const codet &op_code)
Performs a typecheck on a STL instruction that uses two accumulator entries.
void add_temp_rlo()
Adds a symbol for the RLO to the symbol table.
void typecheck_statement_list_xor_not(const codet &op_code, const symbolt &tia_element)
Performs a typecheck on a STL boolean XOR Not instruction.
void typecheck_statement_list_or_not(const codet &op_code, const symbolt &tia_element)
Performs a typecheck on a STL boolean Or Not instruction.
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const std::string & id2string(const irep_idt &d)
void typecheck_statement_list_accu_int_eq(const codet &op_code)
Performs a typecheck on a STL accumulator equality comparison instruction for integers.
void typecheck_function_var_decls(const statement_list_parse_treet::var_declarationst &var_decls, code_typet::parameterst ¶ms, 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 eleme...
void typecheck_statement_list_accu_real_neq(const codet &op_code)
Performs a typecheck on a STL accumulator inequality comparison instruction for double integers.
void typecheck_statement_list_accu_real_mul(const codet &op_code)
Performs a typecheck on a STL accumulator multiply instruction for reals.
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.
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...
const irep_idt & get_identifier() const
function_blockst function_blocks
List of function blocks this parse tree includes.
const irep_idt name
Name of the module.
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 int...
bool statement_list_typecheck(const statement_list_parse_treet &parse_tree, symbol_tablet &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.
An assumption, which must hold in subsequent code.
Fixed-width bit-vector with two's complement interpretation.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
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 ret...
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.
Binary multiplication Associativity is not specified.
exprt simplify_expr(exprt src, const namespacet &ns)
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 i...
void typecheck_statement_list_accu_real_arith(const codet &op_code)
Performs a typecheck on a STL Accumulator instruction for reals.
void typecheck_instruction_without_operand(const codet &op_code)
Performs a typecheck on an operand-less STL instruction.
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.
std::vector< codet > tokens
Data structure for all tokens of the instruction.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
exprt::operandst argumentst
The Boolean constant false.
void typecheck_statement_list_accu_int_mul(const codet &op_code)
Performs a typecheck on a STL accumulator multiply instruction for integers.
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.
void typecheck_statement_list_accu_dint_neq(const codet &op_code)
Performs a typecheck on a STL accumulator inequality comparison instruction for double integers.
void typecheck_statement_list_accu_int_lt(const codet &op_code)
Performs a typecheck on a STL accumulator less than comparison instruction for integers.
std::size_t get_width() const
const or_exprt & to_or_expr(const exprt &expr)
Cast an exprt to a or_exprt.
var_declarationst var_static
FB-exclusive static variable declarations.
void typecheck() override
Performs the actual typecheck by using the parse tree with which the object was initialized and modif...
void typecheck_statement_list_nesting_closed(const codet &op_code)
Performs a typecheck on a Nesting Closed instruction.
#define STATEMENT_LIST_PTR_WIDTH
Size of pointers in Siemens TIA.
void typecheck_statement_list_nested_or(const codet &op_code)
Performs a typecheck on a nested Or instruction.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Extract member of struct or union.
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.
Intermediate representation of a parsed Statement List file before converting it into a goto program.
exprt value
Initial value of symbol.
exprt typecheck_identifier(const symbolt &tia_element, const irep_idt &identifier)
Performs a typecheck on the given identifier and returns its symbol.
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.
message_handlert * message_handler
Structure type, corresponds to C style structs.
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.
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 int...
void typecheck_accumulator_compare_instruction(const irep_idt &comparison)
Performs a typecheck on an STL comparison instruction.
const statement_list_parse_treet & parse_tree
Parse tree which is used to fill the symbol table.
void initialize_bit_expression(const exprt &op)
Initializes the FC, RLO an OR bits for the scenario when a new boolean instruction was encontered.
std::vector< symbol_exprt > tags
List of tags that were included in the source.
void set(const irep_namet &name, const irep_idt &value)
void typecheck_statement_list_accu_dint_div(const codet &op_code)
Performs a typecheck on a STL accumulator divide instruction for double integers.
void typecheck_statement_list_nested_xor(const codet &op_code)
Performs a typecheck on a nested XOR instruction.
A base class for relations, i.e., binary predicates whose two operands have the same type.
const irep_idt & get_identifier() const
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
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.
Symbol table entry describing a data typeThis is a symbol generated as part of type checking.
void typecheck_statement_list_accu_dint_mul(const codet &op_code)
Performs a typecheck on a STL accumulator divide instruction for double integers.
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.
Every time branching occurs inside of a boolean expression string in STL, the current value of the RL...
const typet & return_type() const
void typecheck_statement_list_xor(const codet &op_code, const symbolt &tia_element)
Performs a typecheck on a STL boolean XOR instruction.
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.
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.
void typecheck_statement_list_and(const codet &op_code, const symbolt &tia_element)
Performs a typecheck on a STL boolean And instruction.
bool can_cast_expr< constant_exprt >(const exprt &base)
Symbol table entry of function parameterThis is a symbol generated as part of type checking.
void typecheck_statement_list_accu_int_div(const codet &op_code)
Performs a typecheck on a STL accumulator divide instruction for integers.
var_declarationst var_inout
Inout variable declarations.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Structure for a simple function in Statement List.
A codet representing an assignment in the program.
var_declarationst var_output
Output variable declarations.
The Boolean constant true.
std::vector< exprt > accumulator
Representation of the accumulator of a TIA element.
irep_idt module
Name of module the symbol belongs to.
virtual bool typecheck_main()
#define CPROVER_ASSERT
Name of the CBMC assert function.
API to expression classes.
bool_typet get_bool_type()
Creates a new type that resembles the 'Bool' type of the Siemens PLC languages.
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 eleme...
irep_idt name
The unique identifier.
functionst functions
List of functions this parse tree includes.
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.
bool can_cast_type< floatbv_typet >(const typet &type)
Check whether a reference to a typet is a floatbv_typet.
const and_exprt & to_and_expr(const exprt &expr)
Cast an exprt to a and_exprt.
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.
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.
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.
#define DATA_BLOCK_TYPE_POSTFIX
Postfix for the type of a data block.
Class for encapsulating the current state of the type check.
bool fc_bit
First Check (Part of the TIA status word).
#define DATA_BLOCK_PARAMETER_NAME
Artificial name for the data block interface of a function block.
Statement List Type Helper.
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 versi...
Data structure for representing an arbitrary statement in a program.
bool or_bit
Or (Part of the TIA status word).
void typecheck_statement_list_accu_dint_add(const codet &op_code)
Performs a typecheck on a STL accumulator add instruction for double integers.