cprover
statement_list_typecheck.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Statement List Language Type Checking
4 
5 Author: Matthias Weiss, matthias.weiss@diffblue.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_STATEMENT_LIST_STATEMENT_LIST_TYPECHECK_H
13 #define CPROVER_STATEMENT_LIST_STATEMENT_LIST_TYPECHECK_H
14 
15 #include <util/symbol_table.h>
16 #include <util/typecheck.h>
17 
19 
31  const statement_list_parse_treet &parse_tree,
32  symbol_tablet &symbol_table,
33  const std::string &module,
34  message_handlert &message_handler);
35 
38 {
39 public:
51  const std::string &module,
53 
56  void typecheck() override;
57 
58 private:
61 
64 
67 
68  // Internal state of the PLC program
69  // TODO: Implement complete status word representation.
70  // See the Siemens documentation for further details.
71 
73  std::vector<exprt> accumulator;
74 
79 
84  bool fc_bit = false;
85 
89  bool or_bit = false;
90 
96  {
99 
101  bool or_bit = false;
102 
105 
107  };
108  using nesting_stackt = std::vector<nesting_stack_entryt>;
109 
113 
114  // High level checks
115 
120  const statement_list_parse_treet::functiont &function);
121 
126  const statement_list_parse_treet::function_blockt &function_block);
127 
130  void typecheck_tag_list();
131 
134  void add_temp_rlo();
135 
142  const statement_list_parse_treet::function_blockt &function_block);
143 
153  const irep_idt &var_property);
154 
165  code_typet::parameterst &params,
166  const irep_idt &function_name,
167  const irep_idt &var_property);
168 
174  const statement_list_parse_treet::tia_modulet &tia_module,
175  symbolt &tia_symbol);
176 
182  const statement_list_parse_treet::tia_modulet &tia_module,
183  symbolt &tia_symbol);
184 
190  const statement_list_parse_treet::instructiont &instruction,
191  symbolt &tia_element);
192 
193  // Load and Transfer instructions
194 
199  const codet &op_code,
200  const symbolt &tia_element);
201 
206  void
207  typecheck_statement_list_transfer(const codet &op_code, symbolt &tia_element);
208 
209  // Arithmetic accumulator instructions (int)
210 
214  void typecheck_statement_list_accu_int_add(const codet &op_code);
215 
219  void typecheck_statement_list_accu_int_sub(const codet &op_code);
220 
224  void typecheck_statement_list_accu_int_div(const codet &op_code);
225 
229  void typecheck_statement_list_accu_int_mul(const codet &op_code);
230 
234  void typecheck_statement_list_accu_int_eq(const codet &op_code);
235 
239  void typecheck_statement_list_accu_int_neq(const codet &op_code);
240 
244  void typecheck_statement_list_accu_int_gt(const codet &op_code);
245 
249  void typecheck_statement_list_accu_int_lt(const codet &op_code);
250 
254  void typecheck_statement_list_accu_int_gte(const codet &op_code);
255 
259  void typecheck_statement_list_accu_int_lte(const codet &op_code);
260 
261  // Arithmetic accumulator instructions (dint)
262 
266  void typecheck_statement_list_accu_dint_add(const codet &op_code);
267 
271  void typecheck_statement_list_accu_dint_sub(const codet &op_code);
272 
276  void typecheck_statement_list_accu_dint_div(const codet &op_code);
277 
281  void typecheck_statement_list_accu_dint_mul(const codet &op_code);
282 
286  void typecheck_statement_list_accu_dint_eq(const codet &op_code);
287 
291  void typecheck_statement_list_accu_dint_neq(const codet &op_code);
292 
296  void typecheck_statement_list_accu_dint_gt(const codet &op_code);
297 
301  void typecheck_statement_list_accu_dint_lt(const codet &op_code);
302 
306  void typecheck_statement_list_accu_dint_gte(const codet &op_code);
307 
311  void typecheck_statement_list_accu_dint_lte(const codet &op_code);
312 
313  // Arithmetic accumulator instructions (real)
314 
318  void typecheck_statement_list_accu_real_add(const codet &op_code);
319 
323  void typecheck_statement_list_accu_real_sub(const codet &op_code);
324 
328  void typecheck_statement_list_accu_real_div(const codet &op_code);
329 
333  void typecheck_statement_list_accu_real_mul(const codet &op_code);
334 
338  void typecheck_statement_list_accu_real_eq(const codet &op_code);
339 
343  void typecheck_statement_list_accu_real_neq(const codet &op_code);
344 
348  void typecheck_statement_list_accu_real_gt(const codet &op_code);
349 
353  void typecheck_statement_list_accu_real_lt(const codet &op_code);
354 
358  void typecheck_statement_list_accu_real_gte(const codet &op_code);
359 
363  void typecheck_statement_list_accu_real_lte(const codet &op_code);
364 
365  // Bit Logic instructions
366 
370  void typecheck_statement_list_not(const codet &op_code);
371 
377  const codet &op_code,
378  const symbolt &tia_element);
379 
384  void
385  typecheck_statement_list_or(const codet &op_code, const symbolt &tia_element);
386 
392  const codet &op_code,
393  const symbolt &tia_element);
394 
400  const codet &op_code,
401  const symbolt &tia_element);
402 
408  const codet &op_code,
409  const symbolt &tia_element);
410 
416  const codet &op_code,
417  const symbolt &tia_element);
418 
422 
426  void typecheck_statement_list_nested_and(const codet &op_code);
427 
431  void typecheck_statement_list_nested_or(const codet &op_code);
432 
436  void typecheck_statement_list_nested_xor(const codet &op_code);
437 
441  void typecheck_statement_list_nested_and_not(const codet &op_code);
442 
446  void typecheck_statement_list_nested_or_not(const codet &op_code);
447 
451  void typecheck_statement_list_nested_xor_not(const codet &op_code);
452 
457  void typecheck_statement_list_nesting_closed(const codet &op_code);
458 
463  void
464  typecheck_statement_list_assign(const codet &op_code, symbolt &tia_element);
465 
469  void typecheck_statement_list_set_rlo(const codet &op_code);
470 
474  void typecheck_statement_list_clr_rlo(const codet &op_code);
475 
480  void typecheck_statement_list_set(const codet &op_code, symbolt &tia_element);
481 
486  void
487  typecheck_statement_list_reset(const codet &op_code, symbolt &tia_element);
488 
489  // Control instructions
490 
495  void
496  typecheck_statement_list_call(const codet &op_code, symbolt &tia_element);
497 
498  // Low level checks
499 
502  void typecheck_statement_list_accu_int_arith(const codet &op_code);
503 
507  void typecheck_statement_list_accu_dint_arith(const codet &op_code);
508 
511  void typecheck_statement_list_accu_real_arith(const codet &op_code);
512 
517  const symbol_exprt &
519 
522  void typecheck_instruction_without_operand(const codet &op_code);
523 
527  void typecheck_binary_accumulator_instruction(const codet &op_code);
528 
535  const codet &op_code,
536  const exprt &rlo_value);
537 
546  const codet &op_code,
547  const symbolt &tia_element,
548  bool negate);
549 
553  void typecheck_accumulator_compare_instruction(const irep_idt &comparison);
554 
559  exprt
560  typecheck_identifier(const symbolt &tia_element, const irep_idt &identifier);
561 
566  void typecheck_CPROVER_assert(const codet &op_code, symbolt &tia_element);
567 
572  void typecheck_CPROVER_assume(const codet &op_code, symbolt &tia_element);
573 
578  void typecheck_called_tia_element(const codet &op_code, symbolt &tia_element);
579 
584  void typecheck_called_function(const codet &op_code, symbolt &tia_element);
585 
590  void
591  typecheck_called_function_block(const codet &op_code, symbolt &tia_element);
592 
600  const std::vector<equal_exprt> &assignments,
601  const code_typet::parametert &param,
602  const symbolt &tia_element);
603 
610  const symbolt &tia_element,
611  const exprt &rhs);
612 
621  const std::vector<equal_exprt> &assignments,
622  const typet &return_type,
623  const symbolt &tia_element);
624 
625  // Helper functions
626 
630  void add_to_or_rlo_wrapper(const exprt &op);
631 
635  void initialize_bit_expression(const exprt &op);
636 
640  void save_rlo_state(symbolt &tia_element);
641 };
642 
643 #endif // CPROVER_STATEMENT_LIST_STATEMENT_LIST_TYPECHECK_H
statement_list_typecheckt::create_instance_data_block_type
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.
Definition: statement_list_typecheck.cpp:217
statement_list_typecheckt::typecheck_statement_list_nested_and_not
void typecheck_statement_list_nested_and_not(const codet &op_code)
Performs a typecheck on a nested And Not instruction.
Definition: statement_list_typecheck.cpp:922
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
statement_list_typecheckt::typecheck_statement_list_and_not
void typecheck_statement_list_and_not(const codet &op_code, const symbolt &tia_element)
Performs a typecheck on a STL boolean And Not instruction.
Definition: statement_list_typecheck.cpp:794
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
statement_list_typecheckt::typecheck_statement_list_reset
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.
Definition: statement_list_typecheck.cpp:1077
statement_list_typecheckt::nesting_stack_entryt::or_bit
bool or_bit
The OR bit's value when the entry was generated.
Definition: statement_list_typecheck.h:101
statement_list_typecheckt::typecheck_statement_list_and_before_or
void typecheck_statement_list_and_before_or()
Performs a typecheck on a STL operand-less Or instruction.
Definition: statement_list_typecheck.cpp:903
statement_list_typecheckt::typecheck_statement_list_accu_int_arith
void typecheck_statement_list_accu_int_arith(const codet &op_code)
Performs a typecheck on a STL Accumulator instruction for integers.
Definition: statement_list_typecheck.cpp:1115
statement_list_typecheckt::typecheck_statement_list_accu_int_gt
void typecheck_statement_list_accu_int_gt(const codet &op_code)
Performs a typecheck on a STL accumulator greater than comparison instruction for integers.
Definition: statement_list_typecheck.cpp:549
statement_list_typecheckt::typecheck_statement_list_not
void typecheck_statement_list_not(const codet &op_code)
Performs a typecheck on a STL boolean NOT instruction.
Definition: statement_list_typecheck.cpp:758
statement_list_typecheckt::typecheck_CPROVER_assert
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.
Definition: statement_list_typecheck.cpp:1309
statement_list_typecheckt::module
const irep_idt module
Name of the module this typecheck belongs to.
Definition: statement_list_typecheck.h:66
statement_list_typecheckt::typecheck_statement_list_nested_or_not
void typecheck_statement_list_nested_or_not(const codet &op_code)
Performs a typecheck on a nested Or Not instruction.
Definition: statement_list_typecheck.cpp:938
statement_list_parse_treet::var_declarationst
std::list< var_declarationt > var_declarationst
Definition: statement_list_parse_tree.h:40
statement_list_typecheckt::typecheck_statement_list_call
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.
Definition: statement_list_typecheck.cpp:1094
typet
The type of an expression, extends irept.
Definition: type.h:29
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:738
statement_list_typecheckt::typecheck_statement_list_accu_real_eq
void typecheck_statement_list_accu_real_eq(const codet &op_code)
Performs a typecheck on a STL accumulator equality comparison instruction for double integers.
Definition: statement_list_typecheck.cpp:716
statement_list_typecheckt::typecheck_statement_list_accu_real_sub
void typecheck_statement_list_accu_real_sub(const codet &op_code)
Performs a typecheck on a STL accumulator subtract instruction for reals.
Definition: statement_list_typecheck.cpp:677
statement_list_typecheckt::typecheck_statement_list_nested_and
void typecheck_statement_list_nested_and(const codet &op_code)
Performs a typecheck on a nested And instruction.
Definition: statement_list_typecheck.cpp:914
statement_list_typecheckt::nesting_stackt
std::vector< nesting_stack_entryt > nesting_stackt
Definition: statement_list_typecheck.h:108
statement_list_typecheckt::typecheck_statement_list_accu_dint_sub
void typecheck_statement_list_accu_dint_sub(const codet &op_code)
Performs a typecheck on a STL accumulator subtract instruction for double integers.
Definition: statement_list_typecheck.cpp:583
statement_list_typecheckt::typecheck_statement_list_assign
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.
Definition: statement_list_typecheck.cpp:1021
statement_list_typecheckt::typecheck_statement_list_accu_int_lte
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.
Definition: statement_list_typecheck.cpp:556
statement_list_typecheckt::typecheck_statement_list_accu_real_add
void typecheck_statement_list_accu_real_add(const codet &op_code)
Performs a typecheck on a STL accumulator add instruction for reals.
Definition: statement_list_typecheck.cpp:664
exprt
Base class for all expressions.
Definition: expr.h:53
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:135
statement_list_typecheckt::symbol_table
symbol_tablet & symbol_table
Reference to the symbol table that should be filled during the typecheck.
Definition: statement_list_typecheck.h:63
statement_list_parse_treet::instructiont
Represents a regular Statement List instruction which consists out of one or more codet tokens.
Definition: statement_list_parse_tree.h:45
statement_list_parse_treet::tia_modulet
Base element of all modules in the Totally Integrated Automation (TIA) portal by Siemens.
Definition: statement_list_parse_tree.h:81
statement_list_typecheckt::typecheck_statement_list_accu_dint_arith
void typecheck_statement_list_accu_dint_arith(const codet &op_code)
Performs a typecheck on a STL Accumulator instruction for double integers.
Definition: statement_list_typecheck.cpp:1136
statement_list_typecheckt::save_rlo_state
void save_rlo_state(symbolt &tia_element)
Saves the current RLO bit to a temporary variable to prevent false overrides when modifying boolean v...
Definition: statement_list_typecheck.cpp:1526
statement_list_typecheckt::nesting_stack_entryt::rlo_bit
exprt rlo_bit
The rlo's value when the entry was generated.
Definition: statement_list_typecheck.h:98
statement_list_typecheckt::rlo_bit
exprt rlo_bit
Result of Logic Operation (Part of the TIA status word).
Definition: statement_list_typecheck.h:78
statement_list_typecheckt::typecheck_statement_list_accu_int_neq
void typecheck_statement_list_accu_int_neq(const codet &op_code)
Performs a typecheck on a STL accumulator inequality comparison instruction for integers.
Definition: statement_list_typecheck.cpp:535
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
statement_list_typecheckt::typecheck_statement_list_instruction
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...
Definition: statement_list_typecheck.cpp:319
statement_list_typecheckt::typecheck_statement_list_accu_int_add
void typecheck_statement_list_accu_int_add(const codet &op_code)
Performs a typecheck on a STL accumulator add instruction for integers.
Definition: statement_list_typecheck.cpp:476
statement_list_typecheckt::typecheck_temp_var_decls
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...
Definition: statement_list_typecheck.cpp:276
statement_list_typecheckt::typecheck_statement_list_accu_real_div
void typecheck_statement_list_accu_real_div(const codet &op_code)
Performs a typecheck on a STL accumulator divide instruction for reals.
Definition: statement_list_typecheck.cpp:703
statement_list_typecheckt::nesting_stack_entryt::nesting_stack_entryt
nesting_stack_entryt(exprt rlo_bit, bool or_bit, codet function_code)
Definition: statement_list_typecheck.cpp:69
statement_list_typecheck
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.
Definition: statement_list_typecheck.cpp:57
statement_list_typecheckt::typecheck_tag_list
void typecheck_tag_list()
Performs a typecheck on the tag list of the referenced parse tree and adds symbols for its contents t...
Definition: statement_list_typecheck.cpp:188
statement_list_parse_treet::function_blockt
Structure for a simple function block in Statement List.
Definition: statement_list_parse_tree.h:148
statement_list_typecheckt::typecheck_statement_list_accu_dint_lte
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...
Definition: statement_list_typecheck.cpp:650
statement_list_typecheckt::typecheck_statement_list_nested_xor_not
void typecheck_statement_list_nested_xor_not(const codet &op_code)
Performs a typecheck on a nested XOR Not instruction.
Definition: statement_list_typecheck.cpp:954
statement_list_typecheckt::typecheck_statement_list_or
void typecheck_statement_list_or(const codet &op_code, const symbolt &tia_element)
Performs a typecheck on a STL boolean Or instruction.
Definition: statement_list_typecheck.cpp:816
statement_list_typecheckt::typecheck_statement_list_accu_int_sub
void typecheck_statement_list_accu_int_sub(const codet &op_code)
Performs a typecheck on a STL accumulator subtract instruction for integers.
Definition: statement_list_typecheck.cpp:489
statement_list_typecheckt::typecheck_CPROVER_assume
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.
Definition: statement_list_typecheck.cpp:1328
statement_list_typecheckt::typecheck_called_tia_element
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.
Definition: statement_list_typecheck.cpp:1347
statement_list_typecheckt::typecheck_statement_list_networks
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.
Definition: statement_list_typecheck.cpp:298
statement_list_typecheckt::typecheck_function_call_arguments
exprt typecheck_function_call_arguments(const std::vector< equal_exprt > &assignments, const code_typet::parametert &param, const symbolt &tia_element)
Checks if the given parameter is inside of the assignment list of a function call and returns the exp...
Definition: statement_list_typecheck.cpp:1425
statement_list_typecheckt::typecheck_statement_list_accu_dint_eq
void typecheck_statement_list_accu_dint_eq(const codet &op_code)
Performs a typecheck on a STL accumulator equality comparison instruction for double integers.
Definition: statement_list_typecheck.cpp:622
statement_list_typecheckt::typecheck_statement_list_accu_int_gte
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.
Definition: statement_list_typecheck.cpp:563
statement_list_typecheckt::typecheck_statement_list_accu_real_gt
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.
Definition: statement_list_typecheck.cpp:737
statement_list_typecheckt::nesting_stack
nesting_stackt nesting_stack
Representation of the nesting stack.
Definition: statement_list_typecheck.h:112
statement_list_typecheckt::nesting_stack_entryt::function_code
codet function_code
OP code of the instruction that generated the stack entry.
Definition: statement_list_typecheck.h:104
statement_list_typecheckt::typecheck_statement_list_accu_real_lt
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.
Definition: statement_list_typecheck.cpp:730
statement_list_typecheckt::typecheck_statement_list_load
void typecheck_statement_list_load(const codet &op_code, const symbolt &tia_element)
Performs a typecheck on a STL load instruction.
Definition: statement_list_typecheck.cpp:440
statement_list_typecheckt::typecheck_binary_accumulator_instruction
void typecheck_binary_accumulator_instruction(const codet &op_code)
Performs a typecheck on a STL instruction that uses two accumulator entries.
Definition: statement_list_typecheck.cpp:1208
statement_list_typecheckt::add_temp_rlo
void add_temp_rlo()
Adds a symbol for the RLO to the symbol table.
Definition: statement_list_typecheck.cpp:204
statement_list_typecheckt::typecheck_statement_list_xor_not
void typecheck_statement_list_xor_not(const codet &op_code, const symbolt &tia_element)
Performs a typecheck on a STL boolean XOR Not instruction.
Definition: statement_list_typecheck.cpp:882
statement_list_typecheckt::typecheck_statement_list_or_not
void typecheck_statement_list_or_not(const codet &op_code, const symbolt &tia_element)
Performs a typecheck on a STL boolean Or Not instruction.
Definition: statement_list_typecheck.cpp:841
statement_list_typecheckt::typecheck_statement_list_accu_int_eq
void typecheck_statement_list_accu_int_eq(const codet &op_code)
Performs a typecheck on a STL accumulator equality comparison instruction for integers.
Definition: statement_list_typecheck.cpp:528
statement_list_typecheckt::typecheck_function_var_decls
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 eleme...
Definition: statement_list_typecheck.cpp:249
statement_list_typecheckt::typecheck_statement_list_accu_real_neq
void typecheck_statement_list_accu_real_neq(const codet &op_code)
Performs a typecheck on a STL accumulator inequality comparison instruction for double integers.
Definition: statement_list_typecheck.cpp:723
statement_list_typecheckt::typecheck_statement_list_accu_real_mul
void typecheck_statement_list_accu_real_mul(const codet &op_code)
Performs a typecheck on a STL accumulator multiply instruction for reals.
Definition: statement_list_typecheck.cpp:690
typecheck.h
statement_list_typecheckt::typecheck_statement_list_accu_dint_gt
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.
Definition: statement_list_typecheck.cpp:643
statement_list_typecheckt::typecheck_function_block_declaration
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...
Definition: statement_list_typecheck.cpp:116
statement_list_parse_tree.h
Statement List Language Parse Tree.
statement_list_typecheckt::typecheck_statement_list_accu_dint_gte
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...
Definition: statement_list_typecheck.cpp:657
statement_list_typecheckt::typecheck_return_value_assignment
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...
Definition: statement_list_typecheck.cpp:1471
statement_list_typecheckt::typecheck_statement_list_set
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.
Definition: statement_list_typecheck.cpp:1060
statement_list_typecheckt::typecheck_function_declaration
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...
Definition: statement_list_typecheck.cpp:165
statement_list_typecheckt::typecheck_statement_list_accu_real_arith
void typecheck_statement_list_accu_real_arith(const codet &op_code)
Performs a typecheck on a STL Accumulator instruction for reals.
Definition: statement_list_typecheck.cpp:1158
statement_list_typecheckt::typecheck_instruction_without_operand
void typecheck_instruction_without_operand(const codet &op_code)
Performs a typecheck on an operand-less STL instruction.
Definition: statement_list_typecheck.cpp:1198
statement_list_typecheckt::typecheck_called_function_block
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.
Definition: statement_list_typecheck.cpp:1413
message_handlert
Definition: message.h:28
statement_list_typecheckt::typecheck_statement_list_accu_int_mul
void typecheck_statement_list_accu_int_mul(const codet &op_code)
Performs a typecheck on a STL accumulator multiply instruction for integers.
Definition: statement_list_typecheck.cpp:502
statement_list_typecheckt::statement_list_typecheckt
statement_list_typecheckt(const statement_list_parse_treet &parse_tree, symbol_tablet &symbol_table, const std::string &module, message_handlert &message_handler)
Creates a new instance of statement_list_typecheckt.
Definition: statement_list_typecheck.cpp:77
statement_list_typecheckt::typecheck_statement_list_accu_dint_neq
void typecheck_statement_list_accu_dint_neq(const codet &op_code)
Performs a typecheck on a STL accumulator inequality comparison instruction for double integers.
Definition: statement_list_typecheck.cpp:629
statement_list_typecheckt::typecheck_statement_list_accu_int_lt
void typecheck_statement_list_accu_int_lt(const codet &op_code)
Performs a typecheck on a STL accumulator less than comparison instruction for integers.
Definition: statement_list_typecheck.cpp:542
statement_list_typecheckt::typecheck
void typecheck() override
Performs the actual typecheck by using the parse tree with which the object was initialized and modif...
Definition: statement_list_typecheck.cpp:89
statement_list_typecheckt::typecheck_statement_list_nesting_closed
void typecheck_statement_list_nesting_closed(const codet &op_code)
Performs a typecheck on a Nesting Closed instruction.
Definition: statement_list_typecheck.cpp:962
statement_list_typecheckt::typecheck_statement_list_nested_or
void typecheck_statement_list_nested_or(const codet &op_code)
Performs a typecheck on a nested Or instruction.
Definition: statement_list_typecheck.cpp:930
statement_list_typecheckt::typecheck_instruction_with_non_const_operand
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.
Definition: statement_list_typecheck.cpp:1185
statement_list_parse_treet
Intermediate representation of a parsed Statement List file before converting it into a goto program.
Definition: statement_list_parse_tree.h:22
statement_list_typecheckt::typecheck_identifier
exprt typecheck_identifier(const symbolt &tia_element, const irep_idt &identifier)
Performs a typecheck on the given identifier and returns its symbol.
Definition: statement_list_typecheck.cpp:1247
statement_list_typecheckt::typecheck_statement_list_set_rlo
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.
Definition: statement_list_typecheck.cpp:1042
messaget::message_handler
message_handlert * message_handler
Definition: message.h:439
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:226
statement_list_typecheckt::typecheck_statement_list_transfer
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.
Definition: statement_list_typecheck.cpp:461
statement_list_typecheckt::typecheck_statement_list_accu_real_gte
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...
Definition: statement_list_typecheck.cpp:751
statement_list_typecheckt::typecheck_accumulator_compare_instruction
void typecheck_accumulator_compare_instruction(const irep_idt &comparison)
Performs a typecheck on an STL comparison instruction.
Definition: statement_list_typecheck.cpp:1174
statement_list_typecheckt::parse_tree
const statement_list_parse_treet & parse_tree
Parse tree which is used to fill the symbol table.
Definition: statement_list_typecheck.h:60
statement_list_typecheckt::initialize_bit_expression
void initialize_bit_expression(const exprt &op)
Initializes the FC, RLO an OR bits for the scenario when a new boolean instruction was encontered.
Definition: statement_list_typecheck.cpp:1519
symbolt
Symbol table entry.
Definition: symbol.h:28
statement_list_typecheckt::typecheck_statement_list_accu_dint_div
void typecheck_statement_list_accu_dint_div(const codet &op_code)
Performs a typecheck on a STL accumulator divide instruction for double integers.
Definition: statement_list_typecheck.cpp:609
statement_list_typecheckt::typecheck_statement_list_nested_xor
void typecheck_statement_list_nested_xor(const codet &op_code)
Performs a typecheck on a nested XOR instruction.
Definition: statement_list_typecheck.cpp:946
code_typet::parametert
Definition: std_types.h:753
statement_list_typecheckt::typecheck_statement_list_accu_dint_mul
void typecheck_statement_list_accu_dint_mul(const codet &op_code)
Performs a typecheck on a STL accumulator divide instruction for double integers.
Definition: statement_list_typecheck.cpp:596
statement_list_typecheckt::typecheck_statement_list_accu_dint_lt
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.
Definition: statement_list_typecheck.cpp:636
statement_list_typecheckt::nesting_stack_entryt
Every time branching occurs inside of a boolean expression string in STL, the current value of the RL...
Definition: statement_list_typecheck.h:96
statement_list_typecheckt::typecheck_statement_list_xor
void typecheck_statement_list_xor(const codet &op_code, const symbolt &tia_element)
Performs a typecheck on a STL boolean XOR instruction.
Definition: statement_list_typecheck.cpp:862
statement_list_typecheckt::typecheck_simple_boolean_instruction_operand
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.
Definition: statement_list_typecheck.cpp:1235
statement_list_typecheckt::typecheck_statement_list_accu_real_lte
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.
Definition: statement_list_typecheck.cpp:744
statement_list_typecheckt::typecheck_statement_list_and
void typecheck_statement_list_and(const codet &op_code, const symbolt &tia_element)
Performs a typecheck on a STL boolean And instruction.
Definition: statement_list_typecheck.cpp:772
statement_list_typecheckt::typecheck_statement_list_accu_int_div
void typecheck_statement_list_accu_int_div(const codet &op_code)
Performs a typecheck on a STL accumulator divide instruction for integers.
Definition: statement_list_typecheck.cpp:515
typecheckt
Definition: typecheck.h:17
symbol_table.h
Author: Diffblue Ltd.
statement_list_parse_treet::functiont
Structure for a simple function in Statement List.
Definition: statement_list_parse_tree.h:129
true_exprt
The Boolean constant true.
Definition: std_expr.h:3955
statement_list_typecheckt::accumulator
std::vector< exprt > accumulator
Representation of the accumulator of a TIA element.
Definition: statement_list_typecheck.h:73
statement_list_typecheckt::typecheck_function_block_var_decls
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...
Definition: statement_list_typecheck.cpp:233
statement_list_typecheckt::add_to_or_rlo_wrapper
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.
Definition: statement_list_typecheck.cpp:1499
statement_list_typecheckt::typecheck_nested_boolean_instruction
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.
Definition: statement_list_typecheck.cpp:1219
statement_list_typecheckt::typecheck_statement_list_clr_rlo
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.
Definition: statement_list_typecheck.cpp:1051
statement_list_typecheckt::typecheck_called_function
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.
Definition: statement_list_typecheck.cpp:1369
statement_list_typecheckt
Class for encapsulating the current state of the type check.
Definition: statement_list_typecheck.h:38
statement_list_typecheckt::fc_bit
bool fc_bit
First Check (Part of the TIA status word).
Definition: statement_list_typecheck.h:84
statement_list_typecheckt::typecheck_function_call_argument_rhs
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...
Definition: statement_list_typecheck.cpp:1456
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35
statement_list_typecheckt::or_bit
bool or_bit
Or (Part of the TIA status word).
Definition: statement_list_typecheck.h:89
statement_list_typecheckt::typecheck_statement_list_accu_dint_add
void typecheck_statement_list_accu_dint_add(const codet &op_code)
Performs a typecheck on a STL accumulator add instruction for double integers.
Definition: statement_list_typecheck.cpp:570