Frama-PLC - Check List

Authors:	P. Baudin and F. Bobot
Institute:	CEA-List, Université Paris-Saclay - Software Safety and Security Lab
License:	Creative Commons Attribution-ShareAlike 4.0 International
Copyright	(C) 2019-2022, CEA LIST

Frama-PLC: A Static Analyser of Source Code for Programmable Logic Controllers

CHECK LIST

Syntactical checks are reported during the first analysis phase of the tool whereas the semantic checks are reported by Frama-C tool during the second phase.

E0 - Information

E0.1 - Log messages

Warns when parsing unknown xml tag elements.

E2 - Inadequate Types (syntactical check)

E2.1 - Equalities and inequalities between durations or reals

Warns on the use of equality = and inequality <> comparisons between durations or reals. Even if the duration type TIME can be seen as an integer by EcoStruxure, such a comparison may be inadequate.

Note: - once a duration is converted into an integer using, for example, time_to_dint, the checker cannot complain any more. Idem for the use of real_to_dint. So, the tool can warn (not yet implemented) on the use of such a conversion function.

E2.2 - Rising and falling edge detections on non-EBOOL variables

Warns on the use of edge detections on on non-EBOOL variables

E4 - Constant expressions (syntactical & semantic check)

E4.1 - Expression that has always the same value (semantics)

Warns on expressions of the generated C code that have always the same value (this value is given by Frama-C).

E4.2 - Section activation variable that has always the same value (semantics)

Warns on section activation variables (leading to executions of section code) that have always the same value (this value is given by Frama-C) during their evaluations.

E4.3 - Transition that has always the same value (semantics)

Warns on transition variables (leading step transitions of Grafcets) that have always the same value (this value is given by Frama-C) during their evaluations.

E4.4 - Approximated floating-point constant (syntactical)

Warns on floating-point constant that cannot be represented exactly in a single decimal point floating number (32 bit format of ANSI/IEEE 754 standard).

E5 - Inadequate interfaces (syntactical & semantic check)

E5.1 - Missing uninitialized inputs (syntactical)

Warns on missing inputs of instance variables that are not assigned nor initialized.

E5.2 - Missing inputs having their own initialization (syntactical)

Warns on missing inputs of instance variables that are not assigned but have their own initialization.

Note: the initialization can be specified by the initial value of the instance variables or else from the data type definition of these instance variables.

E5.3 - Unused outputs (syntactical)

Warns on unused outputs of instance variables when all of them are not connected nor read by program statements.

E5.4 - Common inputs of the tasks MAST and FAST (semantics)

Lists the common inputs of the task Mast and Fast.

E5.5 - Common outputs of the tasks MAST and FAST (semantics)

Lists the common outputs of the task Mast and Fast.

E5.6 - Outputs of the task MAST read by the task FAST (semantics)

Lists the outputs of the task Mast read by the task Fast.

E5.7 - Outputs of the task FAST read by the task MAST (semantics)

Lists the outputs of the task Fast read by the task Mast.

E5.8 - Variable accesses outside authorized sections (syntactical)

Warns on variable accesses performed outside the authorized sections. The acceptable accesses can be specified through the configuration file. By defaut, all variable accesses are considered as acceptable by all sections.

E5.9 - Multiple writing (syntactical)

Warns on variables writen in multiple locations.

Note: imprecise access modes can be obtained when using anonymous parameters in ST function calls. In such a case, the Frama-PLC considers a Rd/Wr access to these parameters.

E6 - Inadequate variable declarations (syntactical check)

E6.1 - Use of direct variables

Warns on the direct uses of direct variables (names starting with a %)

E6.2 - Incomplete reserve

Warns on global variables that - contain a reserve or réserve sub-string contradicting its comment; - do not contain a reserve or réserve sub-string, contradicting its comment.

Note: - these checks are case insensitive.

E7 - Dead code (semantic check)

E7.1 - Unreached Grafcet steps

Warns on Grafcet steps that are never reached.

Note: - the tool does not warn for steps of a Grafcet section that is always disable (that case is reported under reference E7.2).

E7.2 - Main code never executed

Warns on sections, transitions, subroutines and instances (their full code) that are never executed.

Note: - the tool does not warn for transitions outgoing from a Grafcet step that is unreachable (that case is reported under reference E7.1).

E7.3 - Piece of code never executed

Warns on sections, transitions, subroutines and instances containing a piece of C code that is never executed.

E8 - Inadequate Logics (syntactical)

E8.1 - Inadequate uses of labels and jumps

Warns on backward and forward LD jumps. Warns also on labels without any jump to them and on jumps to an undefined label.

E8.2 - Non consecutive set/reset coils

Between two set/reset coils involving the same global variable, no other coils are allowed. The tool warns in such a case.

But, when the two concerned coils are different (a set coil and reset one), the tool does not warn if the distance between them is lesser or equal to 25 LD raws.

The tool warns also when there is set coils without near reset and vice versa.

In the same maner, the tool warns also when there is set coils with faraway reset and vice versa.

E9 - Loop constructs (syntactical)

E9.1 - Use of loop statements

Warns on FOR, WHILE, REPEAT, CONTINUE and EXIT constructs.

A specific warning is given for WHILE and REPEAT loop when the loop condition use an equality test.

E11 - Coding Rules (syntactical and semantic check)

E11.1 - Uncommented (syntactical check)

Warns on the absence of comments for global variables except when they have an owner attribute (related to E11.1).

E11.2 - Empty statement (syntactical check)

Warns on empty - ladder (for SFC transitions, instances and sections) - ST blocks

E11.3 - Scanning order rule (semantic check)

Warns on invalid execution order of the sections of the tasks MAST and FAST.

Note: for each section, a message referenced Info.E11.3 informs whether the section performs read and write accesses to the I/O.

E11.4 - Hazardous comment tags/unclosed (syntactical check)

Warns on unclosed comments or comments (in ST code) using opening or closing comment tags in order to prevent about the way nested comments are implemented as specified by the norm ISO 61131-3 (allowing nested comments) or not.

For example, according to the norm ISO 61131-3, this code contents only comment using two lines:

(* x:=0; (* this is (* a nested comment *)
   x:=1; // that is closed by this next comment tag *)

E11.5 - Statements into comments (syntactical check)

Warns on comments containing ST statements

E11.6 - Use of pragma

Warns on the use of pragma notation in ST code.

E12 - Naming rules

Warns on identifier names that do not comply with the dedicated naming rule.

This is performed by defining regular expressions and the names must match the dedicated regular expression. Dedicated checks on the length of these identifiers are also performed.

These naming rules apply to the following identifiers: - functional entities - MAST and FAST sections - global variables - instance variables (name once instantiated) - subroutines

Notes: - the required intervals for the length of these identifiers are modifiable; - theses checks are not case sensitive; - the same kind of checks could be performed for the following identifiers: * instance types (name before the instantiation - not yet implemented) * formal parameters of instance (not yet implemented) * activation variables of sections (not yet implemented) * transition variables (not yet implemented) * state variables (not yet implemented) * variable types (from the name of the variable - not yet implemented)

Regular expressions are defined using the following usual constructs: - exp* matches the expression zero, one or several times - exp+ matches the expression one or several times - exp? matches the expression once or not at all - . matches any characters - [ chars ] matches one of these characters; ranges are denoted with -, as in ['a'-'z'] - exp1 | exp2 alternative between two expressions - ( exp ) groups the enclosed expression

The common definitions of the regular expressions used into the next subsections are:

space  = [' ' '\t']
digit  = ['0'-'9']
letter = ['a'-'z']
alpha  = digit | letter
ident  = letter ('_' | alpha)*
alpha_ident = alpha ('_' | alpha)*

let fr_charset = "ç"|"à"|"â"|"é"|"è"|"ê"|"ë"|"î"|"ï"|"ô"|"û"|"ù"|"ü"|"œ"|"æ"
let fr_letter  = letter | fr_charset
let fr_alpha   = digit | fr_letter
let fr_ident   = fr_letter (underscore | fr_alpha)*

let fr_word = ('_' | fr_alpha)+
let fr_text = fr_word (space fr_word)*

Note: ’ denotes the tabular character

E12.1 - Functional entity rule

The entity names must match the entity_name regular expression:

entity_prefix1 = "ef"
entity_prefix2 = "e" "f"?

entity_number = digit digit digit?

entity_posfix1 = space+ '-' space+ fr_text
entity_posfix2 = '_' fr_ident

entity_name =
| entity_prefix1 entity_number entity_posfix1
| entity_prefix2 entity_number entity_posfix2

For exemple, the entity name EF00 - Entrées Sorties matches the first rule whereas E22_Général matches the second.

There is no constraint on the length of these names (but they cannot be empty).

But, for the entity names used in the application, the entity numbers are extracted from the entity_number part of the regular expression. These numbers are used as reference for other checks.

E12.2 - Section rule

The MAST and FAST section names must match the section_name regular expression and their length must be in the interval [10..[:

instance_name = ident

Note: - there is no check of the upper bound of their length.

E12.3 - Global variable rule

Global variable names must match the global_variable_name regular expression and their length must be in the interval [5..32]:

variable_prefix1 = "e"
variable_prefix2 = "i"|"q"|"ia"|"qa"

variable_type1 = "e"|"m"|"s"|"ea"|"ed"|"sa"
variable_type2 = '_' ("mes"|"tab")

variable_element1 = "calc"? ("r"|"rot"|"g"|['x' 'y' 'z']['1'-'3']?)+
variable_element2 = "ack_trf_tab"|"ok_trf_tab"
                   |"adr"|"bab"|"bit"|"cab"|"com"|"cpt"|"data"|"def_com"
                   |"def_mesure"|"ech"|"mem"|"mm"|"nb_mesure"|"er_rack"
                   |"etat_mesure"|"start"|"t"|"tgv"|"valeur"|"y"|"zx_tab_mesure"
                   |("mv_sq" digit)|("sq" digit?)

variable_postfix =
| variable_element1 '_' alpha_ident
| variable_element2 '_' alpha_ident

global_variable_name =
| variable_prefix1 entity_number variable_type1? "_reserve"? '_' variable_postfix
| variable_prefix1 entity_number variable_type2? "_reserve"? '_' variable_postfix
| variable_prefix2               variable_type2? "_reserve"? '_' variable_postfix

For global variables matching the prefix variable_prefix1, the entity_number part must be referenced in the used entity numbers of the application.

E12.4 Instance variable rule

Instance variable names (after instantiation) must match the instance_name regular expression and their length must be in the interval [5..32]:

instance_name = ident

E12.5 - Subroutine rule

Subroutine names must match the subroutine_name regular expression and their length must be in the interval [5..32]:

subroutine_prefix = "e"

subroutine_kind1 = "sr"
subroutine_kind2 = "msg"|"raz"

subroutine_postfix = ident

subroutine_name =
| subroutine_prefix entity_number '_' subroutine_kind1 '_' subroutine_postfix
| subroutine_prefix entity_number '_' subroutine_kind2 '_' subroutine_postfix

The entity_number part must be referenced in the used entity numbers of the application.

E12.6 - External function rule

External function names must match the function_name regular expression and their length must be in the interval [1..[:

function_name = ident

E13 - Various Frama-C Properties (syntactical and semantic checking)

E13.1 - Various ACSL properties

Warns of various possible errors (related to ACSL properties) identified by Frama-C.

E13.2 Exclusive aspect of the diverging conditions from a step to OR branches

Reports the unproved assertions ensuring the fact that transition conditions from a step are exclusive.

Notes:

• the name of these assert properties has the form exclusive_OR_branch_from_step__<sfc-step-name>;

• in order to ease this verification, some other properties of the C code are added. The verification of these properties is also performed and may fail even if they are true by construct since they give the semantic of the named transitions or Grafcet. The name of these properties has the form:

• helper_for_sfc_state__<sfc-name>;

• helper_for_transitions__<sfc-transition-name>.

E13.3 - Run-time errors

Warns of possible run-time errors identified by the Eva plug-in of Frama-C.

Note: the name of these properties has the form Eva: <RTE-kind>:.