Go to the documentation of this file.
27 #define STATEMENT_LIST_PTR_WIDTH 64
29 #define TYPECHECK_ERROR 0
30 #define DATA_BLOCK_PARAMETER_NAME "data_block"
32 #define DATA_BLOCK_TYPE_POSTFIX "_db"
34 #define CPROVER_ASSERT CPROVER_PREFIX "assert"
36 #define CPROVER_ASSUME CPROVER_PREFIX "assume"
38 #define CPROVER_TEMP_RLO CPROVER_PREFIX "temp_rlo"
62 const std::string &module,
66 parse_tree, symbol_table, module, message_handler);
75 : rlo_bit(rlo_bit), or_bit(or_bit), function_code(function_code)
124 function_block_sym.
name = function_block.
name;
127 function_block_sym.
mode = ID_statement_list;
142 data_block.base_name = data_block.name;
143 data_block.mode = ID_statement_list;
151 param_sym.
type = param.type();
152 param_sym.
name = param.get_identifier();
155 param_sym.
mode = ID_statement_list;
160 params.push_back(param);
162 fb_type.
set(ID_statement_list_type, ID_statement_list_function_block);
163 function_block_sym.
type = fb_type;
172 function_sym.
name =
function.name;
175 function_sym.
mode = ID_statement_list;
178 function.var_input, params,
function.name, ID_statement_list_var_input);
180 function.var_inout, params,
function.name, ID_statement_list_var_inout);
182 function.var_output, params,
function.name, ID_statement_list_var_output);
185 fc_type.
set(ID_statement_list_type, ID_statement_list_function);
186 function_sym.
type = fc_type;
201 tag_sym.
mode = ID_statement_list;
215 temp_rlo.
mode = ID_statement_list;
224 function_block.
var_input, components, ID_statement_list_var_input);
226 function_block.
var_inout, components, ID_statement_list_var_inout);
228 function_block.
var_output, components, ID_statement_list_var_output);
230 function_block.
var_static, components, ID_statement_list_var_static);
243 const irep_idt &var_name{declaration.variable.get_identifier()};
244 const typet &var_type{declaration.variable.type()};
246 component.set(ID_statement_list_type, var_property);
262 param_sym.
type = declaration.variable.type();
264 "::" +
id2string(declaration.variable.get_identifier());
265 param_sym.
base_name = declaration.variable.get_identifier();
267 param_sym.
mode = ID_statement_list;
271 param.set_identifier(param_sym.
name);
272 param.set_base_name(declaration.variable.get_identifier());
273 param.
set(ID_statement_list_type, var_property);
274 params.push_back(param);
291 temp_sym.
mode = ID_statement_list;
312 for(
const auto &network : tia_module.
networks)
316 for(
const auto &instruction : network.instructions)
326 const irep_idt statement{op_code.get_statement()};
328 if(ID_statement_list_load == statement)
330 else if(ID_statement_list_transfer == statement)
332 else if(ID_statement_list_accu_int_add == statement)
334 else if(ID_statement_list_accu_int_sub == statement)
336 else if(ID_statement_list_accu_int_mul == statement)
338 else if(ID_statement_list_accu_int_div == statement)
340 else if(ID_statement_list_accu_int_eq == statement)
342 else if(ID_statement_list_accu_int_neq == statement)
344 else if(ID_statement_list_accu_int_lt == statement)
346 else if(ID_statement_list_accu_int_gt == statement)
348 else if(ID_statement_list_accu_int_lte == statement)
350 else if(ID_statement_list_accu_int_gte == statement)
352 else if(ID_statement_list_accu_dint_add == statement)
354 else if(ID_statement_list_accu_dint_sub == statement)
356 else if(ID_statement_list_accu_dint_mul == statement)
358 else if(ID_statement_list_accu_dint_div == statement)
360 else if(ID_statement_list_accu_dint_eq == statement)
362 else if(ID_statement_list_accu_dint_neq == statement)
364 else if(ID_statement_list_accu_dint_lt == statement)
366 else if(ID_statement_list_accu_dint_gt == statement)
368 else if(ID_statement_list_accu_dint_lte == statement)
370 else if(ID_statement_list_accu_dint_gte == statement)
372 else if(ID_statement_list_accu_real_add == statement)
374 else if(ID_statement_list_accu_real_sub == statement)
376 else if(ID_statement_list_accu_real_mul == statement)
378 else if(ID_statement_list_accu_real_div == statement)
380 else if(ID_statement_list_accu_real_eq == statement)
382 else if(ID_statement_list_accu_real_neq == statement)
384 else if(ID_statement_list_accu_real_lt == statement)
386 else if(ID_statement_list_accu_real_gt == statement)
388 else if(ID_statement_list_accu_real_lte == statement)
390 else if(ID_statement_list_accu_real_gte == statement)
392 else if(ID_statement_list_not == statement)
394 else if(ID_statement_list_and == statement)
396 else if(ID_statement_list_and_not == statement)
398 else if(ID_statement_list_or == statement)
400 else if(ID_statement_list_or_not == statement)
402 else if(ID_statement_list_xor == statement)
404 else if(ID_statement_list_xor_not == statement)
406 else if(ID_statement_list_and_nested == statement)
408 else if(ID_statement_list_and_not_nested == statement)
410 else if(ID_statement_list_or_nested == statement)
412 else if(ID_statement_list_or_not_nested == statement)
414 else if(ID_statement_list_xor_nested == statement)
416 else if(ID_statement_list_xor_not_nested == statement)
418 else if(ID_statement_list_nesting_closed == statement)
420 else if(ID_statement_list_assign == statement)
422 else if(ID_statement_list_set_rlo == statement)
424 else if(ID_statement_list_clr_rlo == statement)
426 else if(ID_statement_list_set == statement)
428 else if(ID_statement_list_reset == statement)
430 else if(ID_statement_list_nop == statement)
432 else if(ID_statement_list_call == statement)
436 error() <<
"OP code of instruction not found: " << op_code.get_statement()
443 const codet &op_code,
447 expr_try_dynamic_cast<symbol_exprt>(op_code.
op0());
458 error() <<
"Instruction is not followed by symbol or constant" <<
eom;
464 const codet &op_code,
471 error() <<
"Types of transfer assignment do not match" <<
eom;
479 const codet &op_code)
492 const codet &op_code)
505 const codet &op_code)
518 const codet &op_code)
531 const codet &op_code)
538 const codet &op_code)
545 const codet &op_code)
552 const codet &op_code)
559 const codet &op_code)
566 const codet &op_code)
573 const codet &op_code)
586 const codet &op_code)
599 const codet &op_code)
612 const codet &op_code)
625 const codet &op_code)
632 const codet &op_code)
639 const codet &op_code)
646 const codet &op_code)
653 const codet &op_code)
660 const codet &op_code)
667 const codet &op_code)
680 const codet &op_code)
693 const codet &op_code)
706 const codet &op_code)
719 const codet &op_code)
726 const codet &op_code)
733 const codet &op_code)
740 const codet &op_code)
747 const codet &op_code)
754 const codet &op_code)
761 const codet &op_code)
775 const codet &op_code,
797 const codet &op_code,
819 const codet &op_code,
844 const codet &op_code,
865 const codet &op_code,
885 const codet &op_code,
917 const codet &op_code)
925 const codet &op_code)
933 const codet &op_code)
941 const codet &op_code)
949 const codet &op_code)
957 const codet &op_code)
965 const codet &op_code)
970 error() <<
"Wrong order of brackets (Right parenthesis is not preceded by "
978 if(ID_statement_list_and_nested == statement)
989 else if(ID_statement_list_and_not_nested == statement)
1000 else if(ID_statement_list_or_nested == statement)
1005 else if(ID_statement_list_or_not_nested == statement)
1010 else if(ID_statement_list_xor_nested == statement)
1015 else if(ID_statement_list_xor_not_nested == statement)
1024 const codet &op_code,
1032 error() <<
"Types of assign do not match" <<
eom;
1045 const codet &op_code)
1054 const codet &op_code)
1063 const codet &op_code,
1067 const irep_idt &identifier{op.get_identifier()};
1080 const codet &op_code,
1084 const irep_idt &identifier{op.get_identifier()};
1097 const codet &op_code,
1101 const irep_idt &identifier{op.get_identifier()};
1110 error() <<
"Called function could not be found" <<
eom;
1118 const codet &op_code)
1126 type_try_dynamic_cast<signedbv_typet>(accu1.type());
1128 type_try_dynamic_cast<signedbv_typet>(accu2.type());
1133 error() <<
"Operands of integer addition are no integers" <<
eom;
1139 const codet &op_code)
1147 type_try_dynamic_cast<signedbv_typet>(accu1.type());
1149 type_try_dynamic_cast<signedbv_typet>(accu2.type());
1154 error() <<
"Operands of double integer addition are no double integers"
1161 const codet &op_code)
1171 error() <<
"Operands of Real addition do not have the type Real" <<
eom;
1188 const codet &op_code)
1191 expr_try_dynamic_cast<symbol_exprt>(op_code.
op0());
1196 error() <<
"Instruction is not followed by symbol" <<
eom;
1201 const codet &op_code)
1205 error() <<
"Instruction is followed by operand" <<
eom;
1211 const codet &op_code)
1216 error() <<
"Not enough operands in the accumulator" <<
eom;
1222 const codet &op_code,
1223 const exprt &rlo_value)
1238 const codet &op_code,
1246 return negate ? not_op : op;
1269 element_type.get(ID_statement_list_type) ==
1270 ID_statement_list_function_block)
1277 type_try_dynamic_cast<struct_typet>(db_expr.
type().
subtype());
1282 if(member.get_name() == identifier)
1291 element_type.get(ID_statement_list_type) == ID_statement_list_function)
1294 for(
const auto &member : element_type.parameters())
1296 if(member.get_base_name() == identifier)
1307 error() <<
"Identifier could not be found in project" <<
eom;
1312 const codet &op_code,
1316 expr_try_dynamic_cast<equal_exprt>(op_code.
op1());
1325 error() <<
"No assignment found for assertion" <<
eom;
1331 const codet &op_code,
1335 expr_try_dynamic_cast<equal_exprt>(op_code.
op1());
1344 error() <<
"No assignment found for assumption" <<
eom;
1350 const codet &op_code,
1354 const symbolt &called_function{
1359 called_type.get(ID_statement_list_type) == ID_statement_list_function_block)
1361 else if(called_type.get(ID_statement_list_type) == ID_statement_list_function)
1365 error() <<
"Tried to call element that is no function or function block"
1372 const codet &op_code,
1376 const symbolt &called_function_sym{
1378 const symbol_exprt called_function_expr{called_function_sym.symbol_expr()};
1384 error() <<
"Function calls should not address instance data blocks" <<
eom;
1391 std::vector<equal_exprt> assignments;
1392 for(
const auto &expr : op_code.
operands())
1403 if(called_type.return_type().is_nil())
1409 assignments, called_type.return_type(), tia_element)};
1416 const codet &op_code,
1423 error() <<
"Calls to function blocks are not supported yet" <<
eom;
1428 const std::vector<equal_exprt> &assignments,
1437 if(param_name == lhs.get_identifier())
1439 exprt assigned_variable{
1442 if(param_type == assigned_variable.type())
1443 return assigned_variable;
1446 error() <<
"Types of parameter assignment do not match: "
1447 << param.
type().
id() <<
" != " << assigned_variable.type().id()
1453 error() <<
"No assignment found for function parameter "
1462 exprt assigned_operand;
1464 expr_try_dynamic_cast<symbol_exprt>(rhs);
1469 assigned_operand = rhs;
1470 return assigned_operand;
1474 const std::vector<equal_exprt> &assignments,
1475 const typet &return_type,
1481 if(ID_statement_list_return_value_id == lhs.get_identifier())
1484 const exprt assigned_variable{
1486 if(return_type == assigned_variable.type())
1487 return assigned_variable;
1490 error() <<
"Types of return value assignment do not match: "
1491 << return_type.
id() <<
" != " << assigned_variable.type().id()
1497 error() <<
"No assignment found for function return value" <<
eom;
1511 or_wrapper.op1() = and_op;
1516 or_wrapper.
op1() = and_op;
1534 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.
API to expression classes for Pointers.
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.