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/typecheck.h>
16 
18 
19 class symbol_tablet;
20 class symbolt;
21 
33  const statement_list_parse_treet &parse_tree,
34  symbol_tablet &symbol_table,
35  const std::string &module,
36  message_handlert &message_handler);
37 
40 {
41 public:
53  const std::string &module,
55 
58  void typecheck() override;
59 
60 private:
63 
66 
69 
70  // Internal state of the PLC program
71  // TODO: Implement complete status word representation.
72  // See the Siemens documentation for further details.
73 
75  std::vector<exprt> accumulator;
76 
81 
86  bool fc_bit = false;
87 
91  bool or_bit = false;
92 
98  {
101 
103  bool or_bit = false;
104 
107 
109  };
110  using nesting_stackt = std::vector<nesting_stack_entryt>;
111 
115 
119  {
122  const size_t nesting_depth;
123 
126  const bool jumps_permitted;
127 
130  const bool fc_false_required;
131 
139  size_t nesting_depth,
140  bool jumps_permitted,
141  bool fc_false_required);
142  };
143  using stl_labelst = std::unordered_map<irep_idt, stl_label_locationt>;
144 
147 
150  {
151  // TODO: Add source location to the structure.
152  // Requires the source location to be added to the parser in general.
153 
156  const size_t nesting_depth;
157 
159  const bool sets_fc_false;
160 
166  };
168  std::unordered_map<irep_idt, std::vector<stl_jump_locationt>>;
169 
175 
176  // High level checks
177 
182  const statement_list_parse_treet::functiont &function);
183 
188  const statement_list_parse_treet::function_blockt &function_block);
189 
192  void typecheck_tag_list();
193 
196  void add_temp_rlo();
197 
204  const statement_list_parse_treet::function_blockt &function_block);
205 
215  const irep_idt &var_property);
216 
227  code_typet::parameterst &params,
228  const irep_idt &function_name,
229  const irep_idt &var_property);
230 
236  const statement_list_parse_treet::tia_modulet &tia_module,
237  symbolt &tia_symbol);
238 
244  const statement_list_parse_treet::tia_modulet &tia_module,
245  symbolt &tia_symbol);
246 
249 
255  const statement_list_parse_treet::instructiont &instruction,
256  symbolt &tia_element);
257 
261  void typecheck_code(const codet &instruction, symbolt &tia_element);
262 
266  void typecheck_label(const codet &instruction, symbolt &tia_element);
267 
268  // Load and Transfer instructions
269 
274  const codet &op_code,
275  const symbolt &tia_element);
276 
281  void
282  typecheck_statement_list_transfer(const codet &op_code, symbolt &tia_element);
283 
284  // Arithmetic accumulator instructions (int)
285 
289  void typecheck_statement_list_accu_int_add(const codet &op_code);
290 
294  void typecheck_statement_list_accu_int_sub(const codet &op_code);
295 
299  void typecheck_statement_list_accu_int_div(const codet &op_code);
300 
304  void typecheck_statement_list_accu_int_mul(const codet &op_code);
305 
309  void typecheck_statement_list_accu_int_eq(const codet &op_code);
310 
314  void typecheck_statement_list_accu_int_neq(const codet &op_code);
315 
319  void typecheck_statement_list_accu_int_gt(const codet &op_code);
320 
324  void typecheck_statement_list_accu_int_lt(const codet &op_code);
325 
329  void typecheck_statement_list_accu_int_gte(const codet &op_code);
330 
334  void typecheck_statement_list_accu_int_lte(const codet &op_code);
335 
336  // Arithmetic accumulator instructions (dint)
337 
341  void typecheck_statement_list_accu_dint_add(const codet &op_code);
342 
346  void typecheck_statement_list_accu_dint_sub(const codet &op_code);
347 
351  void typecheck_statement_list_accu_dint_div(const codet &op_code);
352 
356  void typecheck_statement_list_accu_dint_mul(const codet &op_code);
357 
361  void typecheck_statement_list_accu_dint_eq(const codet &op_code);
362 
366  void typecheck_statement_list_accu_dint_neq(const codet &op_code);
367 
371  void typecheck_statement_list_accu_dint_gt(const codet &op_code);
372 
376  void typecheck_statement_list_accu_dint_lt(const codet &op_code);
377 
381  void typecheck_statement_list_accu_dint_gte(const codet &op_code);
382 
386  void typecheck_statement_list_accu_dint_lte(const codet &op_code);
387 
388  // Arithmetic accumulator instructions (real)
389 
393  void typecheck_statement_list_accu_real_add(const codet &op_code);
394 
398  void typecheck_statement_list_accu_real_sub(const codet &op_code);
399 
403  void typecheck_statement_list_accu_real_div(const codet &op_code);
404 
408  void typecheck_statement_list_accu_real_mul(const codet &op_code);
409 
413  void typecheck_statement_list_accu_real_eq(const codet &op_code);
414 
418  void typecheck_statement_list_accu_real_neq(const codet &op_code);
419 
423  void typecheck_statement_list_accu_real_gt(const codet &op_code);
424 
428  void typecheck_statement_list_accu_real_lt(const codet &op_code);
429 
433  void typecheck_statement_list_accu_real_gte(const codet &op_code);
434 
438  void typecheck_statement_list_accu_real_lte(const codet &op_code);
439 
440  // Bit Logic instructions
441 
445  void typecheck_statement_list_not(const codet &op_code);
446 
452  const codet &op_code,
453  const symbolt &tia_element);
454 
459  void
460  typecheck_statement_list_or(const codet &op_code, const symbolt &tia_element);
461 
467  const codet &op_code,
468  const symbolt &tia_element);
469 
475  const codet &op_code,
476  const symbolt &tia_element);
477 
483  const codet &op_code,
484  const symbolt &tia_element);
485 
491  const codet &op_code,
492  const symbolt &tia_element);
493 
497 
501  void typecheck_statement_list_nested_and(const codet &op_code);
502 
506  void typecheck_statement_list_nested_or(const codet &op_code);
507 
511  void typecheck_statement_list_nested_xor(const codet &op_code);
512 
516  void typecheck_statement_list_nested_and_not(const codet &op_code);
517 
521  void typecheck_statement_list_nested_or_not(const codet &op_code);
522 
526  void typecheck_statement_list_nested_xor_not(const codet &op_code);
527 
532  void typecheck_statement_list_nesting_closed(const codet &op_code);
533 
538  void
539  typecheck_statement_list_assign(const codet &op_code, symbolt &tia_element);
540 
544  void typecheck_statement_list_set_rlo(const codet &op_code);
545 
549  void typecheck_statement_list_clr_rlo(const codet &op_code);
550 
555  void typecheck_statement_list_set(const codet &op_code, symbolt &tia_element);
556 
561  void
562  typecheck_statement_list_reset(const codet &op_code, symbolt &tia_element);
563 
564  // Program Control instructions
565 
570  void
571  typecheck_statement_list_call(const codet &op_code, symbolt &tia_element);
572 
573  // Logic Control instructions
574 
580  const codet &op_code,
581  symbolt &tia_element);
582 
588  const codet &op_code,
589  symbolt &tia_element);
590 
596  const codet &op_code,
597  symbolt &tia_element);
598 
599  // Low level checks
600 
606 
611  const code_labelt &label,
612  const stl_label_locationt &location);
613 
616  void typecheck_statement_list_accu_int_arith(const codet &op_code);
617 
621  void typecheck_statement_list_accu_dint_arith(const codet &op_code);
622 
625  void typecheck_statement_list_accu_real_arith(const codet &op_code);
626 
631  const symbol_exprt &
633 
636  void typecheck_instruction_without_operand(const codet &op_code);
637 
641  void typecheck_binary_accumulator_instruction(const codet &op_code);
642 
649  const codet &op_code,
650  const exprt &rlo_value);
651 
660  const codet &op_code,
661  const symbolt &tia_element,
662  bool negate);
663 
667  void typecheck_accumulator_compare_instruction(const irep_idt &comparison);
668 
675  void typecheck_label_reference(const irep_idt &label, bool sets_fc_false);
676 
681  exprt
682  typecheck_identifier(const symbolt &tia_element, const irep_idt &identifier);
683 
688  void typecheck_CPROVER_assert(const codet &op_code, symbolt &tia_element);
689 
694  void typecheck_CPROVER_assume(const codet &op_code, symbolt &tia_element);
695 
700  void typecheck_called_tia_element(const codet &op_code, symbolt &tia_element);
701 
706  void typecheck_called_function(const codet &op_code, symbolt &tia_element);
707 
712  void
713  typecheck_called_function_block(const codet &op_code, symbolt &tia_element);
714 
722  const std::vector<equal_exprt> &assignments,
723  const code_typet::parametert &param,
724  const symbolt &tia_element);
725 
732  const symbolt &tia_element,
733  const exprt &rhs);
734 
743  const std::vector<equal_exprt> &assignments,
744  const typet &return_type,
745  const symbolt &tia_element);
746 
747  // Helper functions
748 
752  void add_to_or_rlo_wrapper(const exprt &op);
753 
757  void initialize_bit_expression(const exprt &op);
758 
762  void clear_module_state();
763 
767  void clear_network_state();
768 
772  void save_rlo_state(symbolt &tia_element);
773 };
774 
775 #endif // CPROVER_STATEMENT_LIST_STATEMENT_LIST_TYPECHECK_H
codet representation of a label for branch targets.
Definition: std_code.h:959
std::vector< parametert > parameterst
Definition: std_types.h:541
Data structure for representing an arbitrary statement in a program.
Definition: std_code_base.h:29
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
message_handlert * message_handler
Definition: message.h:439
Intermediate representation of a parsed Statement List file before converting it into a goto program.
std::list< var_declarationt > var_declarationst
Class for encapsulating the current state of the type check.
void typecheck_accumulator_compare_instruction(const irep_idt &comparison)
Performs a typecheck on an STL comparison instruction.
void typecheck_statement_list_accu_real_div(const codet &op_code)
Performs a typecheck on a STL accumulator divide instruction for reals.
std::unordered_map< irep_idt, std::vector< stl_jump_locationt > > label_referencest
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.
symbol_tablet & symbol_table
Reference to the symbol table that should be filled during the typecheck.
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...
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.
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.
const statement_list_parse_treet & parse_tree
Parse tree which is used to fill the symbol table.
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_nesting_closed(const codet &op_code)
Performs a typecheck on a Nesting Closed instruction.
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_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.
void clear_module_state()
Modifies the state of the typecheck to resemble the beginning of a new module.
void typecheck_statement_list_accu_int_add(const codet &op_code)
Performs a typecheck on a STL accumulator add instruction for integers.
void typecheck_jump_locations(const code_labelt &label, const stl_label_locationt &location)
Performs a typecheck on all references for the given label.
void typecheck_label_reference(const irep_idt &label, bool sets_fc_false)
Checks if the given label is already present and compares the current state with it.
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_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_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_dint_gte(const codet &op_code)
Performs a typecheck on a STL accumulator greater than or equal comparison instruction for double int...
void typecheck_statement_list_and_not(const codet &op_code, const symbolt &tia_element)
Performs a typecheck on a STL boolean And Not instruction.
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.
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...
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...
void typecheck() override
Performs the actual typecheck by using the parse tree with which the object was initialized and modif...
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_int_gte(const codet &op_code)
Performs a typecheck on a STL accumulator greater than or equal comparison instruction for integers.
void typecheck_statement_list_nested_xor(const codet &op_code)
Performs a typecheck on a nested XOR instruction.
void typecheck_statement_list_accu_int_mul(const codet &op_code)
Performs a typecheck on a STL accumulator multiply instruction for integers.
const irep_idt module
Name of the module this typecheck belongs to.
void typecheck_statement_list_accu_int_lt(const codet &op_code)
Performs a typecheck on a STL accumulator less than comparison instruction for integers.
void typecheck_statement_list_nested_or_not(const codet &op_code)
Performs a typecheck on a nested Or Not instruction.
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.
void typecheck_statement_list_accu_dint_add(const codet &op_code)
Performs a typecheck on a STL accumulator add instruction for double integers.
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.
std::vector< exprt > accumulator
Representation of the accumulator of a TIA element.
void typecheck_statement_list_nested_xor_not(const codet &op_code)
Performs a typecheck on a nested XOR Not instruction.
void clear_network_state()
Modifies the state of the typecheck to resemble the beginning of a new network.
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 typecheck_statement_list_xor(const codet &op_code, const symbolt &tia_element)
Performs a typecheck on a STL boolean XOR instruction.
std::unordered_map< irep_idt, stl_label_locationt > stl_labelst
exprt typecheck_identifier(const symbolt &tia_element, const irep_idt &identifier)
Performs a typecheck on the given identifier and returns its symbol.
void typecheck_tag_list()
Performs a typecheck on the tag list of the referenced parse tree and adds symbols for its contents t...
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_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.
void typecheck_statement_list_jump_unconditional(const codet &op_code, symbolt &tia_element)
Performs a typecheck on an unconditional jump instruction (JU) and adds the jump to the given symbol.
void typecheck_code(const codet &instruction, symbolt &tia_element)
Performs a typecheck for the specified instruction in code form.
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_statement_list_accu_real_add(const codet &op_code)
Performs a typecheck on a STL accumulator add instruction for reals.
label_referencest label_references
Holds associations between labels and jumps that are referencing it.
exprt rlo_bit
Result of Logic Operation (Part of the TIA status word).
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.
bool or_bit
Or (Part of the TIA status word).
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.
stl_labelst stl_labels
Data structure that contains data about the labels of the current module.
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...
void typecheck_statement_list_load(const codet &op_code, const symbolt &tia_element)
Performs a typecheck on a STL load instruction.
void typecheck_statement_list_accu_int_div(const codet &op_code)
Performs a typecheck on a STL accumulator divide instruction for integers.
stl_label_locationt typecheck_label_location(const code_labelt &label)
Converts the properties of the current typecheck state to a label location.
void typecheck_statement_list_accu_int_neq(const codet &op_code)
Performs a typecheck on a STL accumulator inequality comparison instruction for integers.
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_arith(const codet &op_code)
Performs a typecheck on a STL Accumulator 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.
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_instruction_without_operand(const codet &op_code)
Performs a typecheck on an operand-less STL instruction.
void typecheck_label(const codet &instruction, symbolt &tia_element)
Performs a typecheck for the given label in code form.
bool fc_bit
First Check (Part of the TIA status word).
void typecheck_statement_list_jump_conditional(const codet &op_code, symbolt &tia_element)
Performs a typecheck on a conditional jump instruction (JC) and adds it to the given symbol.
void typecheck_statement_list_jump_conditional_not(const codet &op_code, symbolt &tia_element)
Performs a typecheck on a inverted conditional jump instruction (JCN) and adds it to the given symbol...
void typecheck_statement_list_or_not(const codet &op_code, const symbolt &tia_element)
Performs a typecheck on a STL boolean Or Not instruction.
void typecheck_label_references()
Checks if all jumps reference labels that exist.
void typecheck_binary_accumulator_instruction(const codet &op_code)
Performs a typecheck on a STL instruction that uses two accumulator entries.
void initialize_bit_expression(const exprt &op)
Initializes the FC, RLO an OR bits for the scenario when a new boolean instruction was encontered.
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.
void typecheck_statement_list_nested_or(const codet &op_code)
Performs a typecheck on a nested Or instruction.
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_real_mul(const codet &op_code)
Performs a typecheck on a STL accumulator multiply instruction for reals.
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_dint_arith(const codet &op_code)
Performs a typecheck on a STL Accumulator instruction for double integers.
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.
void typecheck_statement_list_nested_and_not(const codet &op_code)
Performs a typecheck on a nested And Not instruction.
void typecheck_statement_list_accu_int_gt(const codet &op_code)
Performs a typecheck on a STL accumulator greater than comparison instruction for integers.
void typecheck_statement_list_accu_int_sub(const codet &op_code)
Performs a typecheck on a STL accumulator subtract instruction for integers.
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...
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_dint_eq(const codet &op_code)
Performs a typecheck on a STL accumulator equality comparison instruction for double integers.
void typecheck_statement_list_accu_real_arith(const codet &op_code)
Performs a typecheck on a STL Accumulator instruction for reals.
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_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.
void typecheck_statement_list_accu_real_neq(const codet &op_code)
Performs a typecheck on a STL accumulator inequality comparison instruction for double integers.
nesting_stackt nesting_stack
Representation of the nesting stack.
void typecheck_statement_list_not(const codet &op_code)
Performs a typecheck on a STL boolean NOT instruction.
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...
std::vector< nesting_stack_entryt > nesting_stackt
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.
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.
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_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_eq(const codet &op_code)
Performs a typecheck on a STL accumulator equality comparison instruction for integers.
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_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.
void typecheck_statement_list_accu_dint_div(const codet &op_code)
Performs a typecheck on a STL accumulator divide instruction for double integers.
void add_temp_rlo()
Adds a symbol for the RLO to the symbol table.
void typecheck_statement_list_nested_and(const codet &op_code)
Performs a typecheck on a nested And instruction.
void save_rlo_state(symbolt &tia_element)
Saves the current RLO bit to a temporary variable to prevent false overrides when modifying boolean v...
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_set(const codet &op_code, symbolt &tia_element)
Performs a typecheck on a STL 'S' instruction and saves the result to the given 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_and_before_or()
Performs a typecheck on a STL operand-less Or instruction.
Structure type, corresponds to C style structs.
Definition: std_types.h:231
std::vector< componentt > componentst
Definition: std_types.h:140
Expression to hold a symbol (variable)
Definition: std_expr.h:80
The symbol table.
Definition: symbol_table.h:14
Symbol table entry.
Definition: symbol.h:28
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
The Boolean constant true.
Definition: std_expr.h:2856
The type of an expression, extends irept.
Definition: type.h:29
Statement List Language Parse Tree.
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.
Structure for a simple function block in Statement List.
Structure for a simple function in Statement List.
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.
Every time branching occurs inside of a boolean expression string in STL, the current value of the RL...
nesting_stack_entryt(exprt rlo_bit, bool or_bit, codet function_code)
exprt rlo_bit
The rlo's value when the entry was generated.
codet function_code
OP code of the instruction that generated the stack entry.
bool or_bit
The OR bit's value when the entry was generated.
Holds information about the properties of a jump instruction.
const size_t nesting_depth
The size of the nesting stack at the label location, used for checking scope violations.
stl_jump_locationt(size_t nesting_depth, bool sets_fc_false)
Constructs a new location with the specified properties.
const bool sets_fc_false
States if the jump instruction sets the /FC bit to false.
Holds information about the instruction and the nesting depth to which a label points.
const bool jumps_permitted
States if jumps to this location are permitted or if the location is invalid.
const size_t nesting_depth
The size of the nesting stack at the label location, used for checking scope violations.
stl_label_locationt(size_t nesting_depth, bool jumps_permitted, bool fc_false_required)
Constructs a new location with the specified properties.
const bool fc_false_required
States if jump instructions to this location need to set the /FC bit to false.