Frama-PLC: User’s Manual

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.

1. Archive Overview and Installation.

Archive overview.

The Frama-PLC distribution is separated into two Zip archives. The main archive contains the Windows binaries necessary to performs the syntactical and semantic checks of PLC application software while the second one contains a viewer to navigate into the reported checks and classify them.

All files are located in the /home/framac directory of the main Zip archive. The binaries of the tools are located in its .opam sub-directory. The frama-plc-share sub-directory contains the main informative files:

INSTALL - installation procedure
LICENSE - licensing information
CHANGES - changes information between Frama-PLC versions
doc/Frama-PLC-user-manual.pdf - this document
doc/Frama-PLC-check-list.pdf - a list of the performed checks
doc/Frama-PLC-installation-guide.pdf - a PDF version of the INSTALL file
scripts/run-frama-plc-*.bat - some Windows Batch scripts that are front-ends to frama-plc.sh script
scripts/*.bat - some other Windows Batch scripts
scripts/frama-plc.sh - a Unix script that is a front end to frama-plc-checker.exe tool
scripts/*.sh - some other Unix scripts
scripts/frama-plc.ml - a generic OCaml file used by the frama-plc-checker.exe tool
tests/Frama-PLC.cfg - a configuration file giving the list of all modifiable parameters
tests/*/*.zef - some PLC applications used for testing Frama PLC tools
tests/*/*.cfg - some specific configuration files dedicated to PLC applications
tests/*/*.fos - some specific filter-out specification files dedicated to PLC applications

Installation procedure.

follows the procedure described into the installation guide (c.f. doc/Frama-PLC-installation-guide.pdf).

2. Guidelines for the Procedure of Use

The Frama-PLC tool performs syntactical and semantic checks of PLC application software. Syntactical checks are reported during the first analysis step whereas the semantic checks are reported during the second step.

The list of the checks performed by the Frama-PLC tools is described into the Check List document (c.f. doc/Frama-PLC-check-list.pdf).

Process Guidelines.

Performs the syntactical and semantic checks of the PLC application software using Frama-PLC back-ends (c.f. section 2.2.1) or front-ends (c.f. section 2.2.2).
Runs the viewer tool to navigates into the reported checks and classifies them (c.f. section 2.1)

2.1 Result analysis from the JavaScript platform

The viewer of the analysis results of Frama-PLC checker is available in JavaScript. It is supported by some browsers such as Firefox and Chrome for multiple platforms. Unfortunately, the Windows Internet explorer does not support this JavaScript tool.

Process Guidelines.

Runs the Syntactical checker tool from an HTML browser in opening the file Frama-PLC/Frama-PLC.html:

chooses a report file. The results of an analysis are saved into Json (JavaScript Object Notation format) files. The .json1 extension is used for files that content syntactical analysis reports while the .json2 is used for the semantic analysis report files. Files with a .json extension contents the merge of both analyses. Clicks on the Import button of the section Reporting and selects the report file to examine;
navigates into the reported checks and the application from clicks on the bullets in front of the items. That unfolds the selected item of one step. Clicks eventually on the new items that appeared in order to unfold them as much as possible;
load declassification filters. These filters can be specified into the filters_out parameter (c.f. section 3.1) of a configuration file (files with a .cfg extension) or directly into a declassification file (c.f. section 4, files with a .fos extension). Clicks on the Import button of the section Declassification filter and selects a configuration file or a filter-out specification file;
classifies the reported checks.
save the current declassification fiters. Clicks on the export button. That creates (or updates) an HTML link. Clicks on that new link to save the filter-out rules into a declassification file.

2.2 From Linux/Cygwin platforms

2.2.1 Back-ends

The Syntactical and semantic checker have a command line interface for Linux/Cygwin platforms. The main tool frama-plc-checker.exe is packaged using Opam (a package manager for development in OCaml language) and delivered into the .opam directory of the archive (as Frama-C tool used in back-end for the semantic analysis).

Synopsis of a command line.

The command lines have to be executed into a Linux/Cygwin console. They have the following forms:

frama-plc-checker [commands] [options] <App.xef>
frama-plc-checker --help

Note: the last command shows an help to the standard output describing the different commands and options.

Process guidelines.

The process of a complete analysis can be decomposed into five steps:

Parses the XML application file <App.xef> (or <App.zef>) and reports the syntactic checks into a Json file <App.json1>:
- frama-plc-checker.exe --json1 <App.xef>
Converts the XML application file into a C file <App.c>:
- frama-plc-checker.exe -c [mem-inputs-options] <App.xef>
Builds from the XML application file a dedicated Ocaml script <App.ml> for Frama-C:
- frama-plc-checker.exe --ml [mem-inputs-options] [order-options] <App.xef>
Performs a static analysis of the generated C file, reporting rounding errors of floating point constants (optional), and saves the result into an intermediate file <App.saved> (be very patient):
- frama-c -eva [eva-options] -inout [inout-options] <App.c> -then -wp [wp-options] -then -save <App.saved>
Reports the semantic checks into a Json file <App.json2>
- frama-c -load <App.saved> -load-script <App.ml>
Parses the XML application file <App.xef> (or <App.zef>) and reports the syntactic and merge checks semantic <App.json2> into a Json file <App.json>:
- frama-plc-checker.exe --json <App.xef>

The steps 4 and 5 require the use of Frama-C. This use can be performed using the command line interface:

Steps 2 and 4 in one command:
- frama-plc-checker.exe -c [mem-inputs-options] --analysis <App.xef>
Steps 2 to 5 in one command:
- frama-plc-checker.exe -c [mem-inputs-options] --ml [order-options] --analysis --json2 <App.xef>
Steps 1 and 6 in one command (when steps 2 to 5 have been performed) :
- frama-plc-checker.exe --json1 --json <App.xef>

Note: Json reports generated by the steps 1, 5 or 6 can be examined via an HTML browser in opening the file Frama-PLC/Frama-PLC.html.

Note: the tool frama-plc-checker.exe reuses the basename of the application for naming the generated files. But, the name of the OCaml script have to be compliant with the rule of the OCaml programming language (its basename must start by an alphabetic letter that may be followed by alpha-numeric or underscore characters). So, all non alpha-numeric characters of the application basename are automatically replaced by underscores to get the basename of the generated files. The option --dst-basename <string> allows to select the string used as basename of the generated files.

Options related to the application environment.

The [mem-inputs-options] used at step 3 must be identical to the one used at step 2. These options specify whether the semantic analysis considers the topological variables %M<num> and %MW<num> as modifiable by the environment or not (not means they are only explicitly modifiable by the application):

--mem-is-input=false: the environment do not modify any %M nor %MW variables. The option value defaults to true (%M and %MW variables are modifiable by the environment);
--mem-not-input=<num>: the environment do not modify the%M` variable. A multiple use of this option defines a set of variables to consider;
--memw-not-input=<num>: the environment do not modify the%MW` variable. A multiple use of this option defines a set of variables to consider.

So, these options are very specific to the analyzed PLC application. They have to be specified into a specific configuration file dedicated to the PLC application.

Options related to the section order checking (c.f. E11.3).

The [order-options] used at step 4 specify the required order of the sections of the tasks Mast and Fast. The information is stored into the generated OCaml script and the proper checks are performed at step 5:

--re-mast-order and --re-fast-order options defines two regular expressions allowing the verification of the execution order of the sections of the tasks Mast and Fast.

These regular expressions are defined using the following usual constructs:

. matches any characters
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
exp1 | exp2 alternative between two expressions
( exp ) groups the enclosed expression

The verification principle is the following: lets

the section sequence S_1, …, S_n be the execution order of the sections of a task,
the section S_i be related to the functionnal entity EFxx_i,

and considers the new sequence obtained by substitution of each section S_i by their related EFxx_i.

The execution order is valid when this new sequence matches the given regular expression.

In order to take into account that, only the first sections are allowed to access to the inputs (and that only the last ones are allowed to access to the outputs), an extra post-fix (composed of two characters) is added to each EFxx_i:

-- is added to sections performing no access to inputs nor outputs
-w is added to sections performing no access to inputs
r- is added to sections performing no access to outputs
rw is added to sections that may perform accesses to inputs or outputs

For example, the option --re-fast-order="(EF00r-)+(EF..--)*(EF00-w)+" validate an execution order of sections of the Fast task that consists of:

several successive sections (at least one) related to EF00 and allowed to access to inputs only,
followed by eventual sections related to EF.. (any entity number) and performing no access to inputs nor outputs,
followed by several successive sections (at least one) related to EF00 and allowed to access to outputs only.

Frama-C options.

The step 4 performs a static analysis of the C file that relies on plug-in Eva, InOut and Wp of Frama-C. The combination of these three analyses takes a long time (be patient) Their recommended options are the following (see the related manuals):

Eva options: -eva-precision=1 -eva-no-print
InOut options: -inout-callwise -inout-no-print
Wp options: -wp-cache=update -wp-prop=wp -wp-timeout=2 -wp-msg-key=success-only -wp-prover=alt-ergo,cvc4

2.2.2 Front-ends

Front-end to the main command line tool.

The archive contents a Batch script file for Windows platform that is a front-end to the main command line tool:

scripts/run-frama-plc-script.bat

It is possible to drag and drop a PLC application file into this Batch file. That opens a Cygwin terminal and runs the main command line tool via an intermediate Unix Bash script. By default, the resulting files are stored in the same directory of the PLC application file.

The actions ordered by the Windows Batch script are exchanged with the Unix Bash script through environment variables:

FRAMA_PLC_SHARE - path to frama-plc-share directory of the archive;
FRAMA_PLC_APPLICATION - the PLC application file to analyse;
FRAMA_PLC_DESTDIR - location directory for issued files (defaults to the directory that contents the PLC application file to analyse);
FRAMA_PLC_CONFIG - the configuration file to use (defaults to an eventual configuration file dedicated to the PLC application file to analyse. It should be into same directory, with the same basename, but with a .cfg extension or else named Frama-PLC.cfg);
FRAMA_PLC_FILTER - the filter-out specification file used for the declassification of the reported checks (defaults to an eventual configuration file dedicated to the PLC application file to analyse. It should be into same directory, with the same basename, but with a .fos extension). That allows to overload the parameter given into the configuration file);
FRAMA_PLC_OPTIONS - options redirected to the command line running frama-plc-checker.exe tool (mainly for debugging purpose).

3. Configuration file

The Configuration file has the following Json (JavaScript Object Notation) format:

BNF grammar of configuration files:

configuration	:	`'{'` parameters? `'}'`;
parameters	:	parameter ( `','` parameters )*;
parameter	:	parameter-name `':'` value;
parameter-name	:	string;
value	:	literal
	`\|`	value-enum
	`\|`	value-list;
value-enum	:	`'[` string `']'`;
value-list	`\|`	`'['` values? `']'`;
values	:	value ( `','` value )*;
literal	:	boolean
	`\|`	integer
	`\|`	string;

Syntax of the literals (terminal elements):

boolean	:	`'true'` `\|` `'false'`
integer	:	[`0`..`9`]+
string	:	javascript string literal
		see https://javascript.info/string

3.1 Parameter names & value types

Parameters related to the application environment model.

These options specify whether the semantic analysis considers the topological variables %M<num> and %MW<num>:

"mem_is_input" : boolean: Defaults to true. That models the fact that the application environment is allowed to modified %M and %MW variables, except the ones listed in "mem_not_inputs" or "memw_not_inputs" parameters, except for these listed into "mem_not_inputs" and "memw_not_inputs" parameters.; Set the parameter to false requires that the application environment does not change the values of %M and %MW variables (only the application can directly modify them).; The parameter can be overloaded using the --mem-is-input option of the command line.

"mem_not_inputs" : integer list: Defaults to the empty list.; The parameter requires, for each listed <number>, that the application environment does not change the %M<number> variable.; The parameters can be overloaded using the --mem-not-inputs option of the command line.

"memw_not_inputs" : integer list: Defaults to the empty list.; The parameter requires, for each listed <number>, that the application environment does not change the %MW<number> variable.; The parameters can be overloaded using the --memw-not-inputs option of the command line.

See section 2.2.1 about the “options related to the application environment” for some more explanation.

Classification parameters.

"filters_out" : string list: Defaults to [ "E1.1.*", "Jump_missing", "E5.4.*", "E5.5.*", "E5.6.*", "E5.7.*";"Constant_expression" ] (declassifying logs, alarms related to the presence of LD labels without goto statements, …).; Each string of the list can be either the name a Json file specifying the checks that can be declassified or an identifier related to the kind of alarms to declassify.; The Json format allows also to perform declassification according to pattern related to the context of the reported checks.; The parameters can be overloaded using the --filter-out option of the command line.

See section 4 about the “Declassification” for more details.

Parameters relater to scanning order rules (c.f. checks E11.3).

"mast_regexp_order" : reg-exp list: Defaults to the list [ "(EF00r-)+", "(EF..--)+", "(EF00-w)+" ].; The parameters can be overloaded using the --mast-regexp-order option of the command line.

"fast_regexp_order" : reg-exp list: Defaults to the list [ "(EF00r-)+", "(EF..--)+", "(EF00-w)+" ].; The parameters can be overloaded using the --fast-regexp-order option of the command line.

See section 2.2.1 about the “options related to the section order checking” for the syntax description of the regular expression (regexp) and the performed checks.

Parameters related to consecutive set/reset coils (c.f. checks E8.2).

"maxrow_set_reset_coil" : integer: Defaults to 25.

Parameters related to length of identifiers (c.f. checks E12).

"minlen_section" : integer: Defaults to 10.; Minimal length required for the identifiers of sections.

"maxlen_section" : integer: Defaults to 0 (no constraint on the maximal length).; Maximal length required for the identifiers of sections.

"minlen_instance" : integer: Defaults to 5.; Minimal length required for the identifiers of instance variables.

"maxlen_instance" : integer: Defaults to 32.; Maximal length required for the identifiers of instance variables.

"minlen_global" : integer: Defaults to 5.; Minimal length required for the identifiers of global variables.

"maxlen_global" : integer: Defaults to 32.; Maximal length required for the identifiers of global variables.

"minlen_subroutine" : integer: Defaults to 5.; Minimal length required for the identifiers of subroutines.

"maxlen_subroutine" : integer: Defaults to 32.; Maximal length required for the identifiers of subroutines.

"minlen_function" : integer: Defaults to 1.; Minimal length required for the identifiers of external functions.

"maxlen_function" : integer: Defaults to 0 (no constraint on the maximal length).; Maximal length required for the identifiers of external functions.

Parameters related to naming rules (c.f. checks E12).

"regexp_entity" : naming-rule list: List of naming rules that must satisfy functional entity identifiers.

"regexp_section" : naming-rule list: List of naming rules that must satisfy section identifiers.

"regexp_instance" : naming-rule list: List of naming rules that must satisfy instance identifiers.

"regexp_global" : naming-rule list: List of naming rules that must satisfy golbal variable identifiers.

"regexp_subroutine" : naming-rule list: List of naming rules that must satisfy subroutine identifiers.

"regexp_function" : naming-rule list: List of naming rules that must satisfy external function identifiers.

All rules of the specified list must be satisfied for the considered identifiers. The grammar of a list of naming rules is the following:

list-of-naming-rules	:	`'['` naming-rules? `']'`;
naming-rules	:	naming-rule ( `','` naming-rule )*;
naming-rule	:	‘[’ group ( `','` group )* ’]’
group	:	`'['` group-name `','` reg-exp `']'`
group-name	:	string
reg-exp	:	string

A naming rule is composed of an ordered list of groups; and a group is composed of a name and a regular expression.

When a naming rule is composed of only one group, the considered identifier must match the associated regular expression, from the first character of the identifier to its final character. For example, lets consider the following naming rule used to check functional entity names:

[ [ "incorrect prefix", "[a-z]+[0-9].*" ] ]

The group name incorrect prefix is part of the error message given for functional entity names such that the entity number is not prefixed by some letters. The pattern .* accepts all characters next to the number until the end of the identifier.

When a naming rule is composed of several groups, the first characters of the considered identifier must match the regular expression of the first group and the remaining characters must match the remaining groups of the rule; recursively until the end of the identifier and the final group. For example, lets consider the following naming rule used to check subroutine identifiers:

[ [ "incorrect prefix", "e[0-9]+_" ],

[ "incorrect kind", "(sr|msg|raz)_" ],

[ "incorrect post-fix", "[a-z0-9][_a-z0-9]*" ] ]

The subroutine identifier must be composed of a prefix, followed by a kind and ended by a post-fix. So, the group name incorrect prefix is part of the error message given for subroutine identifiers that do not start with an "e" followed by any number ([0-9]+) and an underscore (_).

Then, the remaining characters must start by “sr_” or “msg_” or “raz_” (otherwise an error message with be raised and contains the explanation incorrect kind) and ends by the specified post-fix.

Parameters related to functional entity numbers (c.f. E12).

"regexp_entity_number" : reg-exp: Defaults to "^[a-z]+([0-9][0-9]+)".; Regular expression used to extract the entity number from functional entity identifiers.

"regexp_global_number" : reg-exp: Defaults to "^e([0-9]+)".; Regular expression used to extract the entity numbers referenced by the global variable identifiers.

"regexp_subroutine_number" : reg-exp: Defaults to "^e([0-9]+)".; Regular expression used to extract the entity numbers referenced by the subroutine identifiers.

The numbers are extracted from the text matching the part of the regexp enclosed by the first parenthesis.

Parameters related to the control of the variable accesses (c.f. E5.8).

"regexp_variable_access_outside_section" : unacceptable-access list: Defaults to [ ]; The unacceptable-access is a list containing a boolean followed by two regular expressions (the first one is dedicated to variable names and the second to section names). The empty list (the default value of the option) specifies no unacceptable-access.

The grammar of a list of unacceptable accesses is the following:

list-of-unacceptable-accesses	:	`'['` unacceptable-accesses? `']'`;
unacceptable-accesses	:	unacceptable-access ( `','` unacceptable-access )*;
unacceptable-access	:	‘[’ access-mode `','` unacceptable-variables `','` acceptable-sections ’]’;
*access-mode	:	bool;
unacceptable-variables	:	regexp;
acceptable-sections	:	regexp;

An unacceptable variable access is for a variable whose name matches the regular expression dedicated to the unacceptable variables and whose access is outside sections matching the regular expression dedicated to the acceptable sections. When the boolean is true, only the write accesses can be unacceptable. The accesses of variables whose name do not match one of the regular expression dedicated to unacceptable variables of the list are acceptable.

When the given regular expression for unacceptable variables cannot be understood by the Frama-PLC (i.e. due to a syntax error in the regular expression) it uses the value ".*" as regular expression such that all variables can be considered unacceptable. For the regular expression dedicated to acceptable section, in such a case Frama-PLC uses the value "" such that there is no acceptable section.

The value [ [ false, ".*", "" ] ] is such that all variable names match the ".*" regular expression and no section match the "" regular expression. Since the boolean value is false, all variable accesses are unacceptable and reported as an E5.8 alarm. With a true value for that boolean, only write accesses are unacceptable.

There are some logical properties about the acceptable_access list - [ [ b, "regexp1", "regexp" ], [ b, "regexp2", "regexp" ] ] is equivalent to [ [ b, "(regexp1)|(regexp2)", "regexp" ] ] - [ [ b, "regexp", "regexp1" ], [ b, "regexp", "regexp2" ] ] is equivalent to [ [ b, "regexp", "(regexp1)|(regexp2)" ] ]

Note: the list [ [ false, ".*", ".*" ] ] is similar to the empty list because all section names match the ".*" regular expression dedicated to acceptable sections (so, all variable accesses are in acceptable sections).

Parameters related to Frama-PLC parser

"lexing_comment_style" : enum value among "Nested" and "Simple": Defaults to [ "Simple" ].; Options specifying how the comments present into ST source code are parsed. For example, within the Simple style, the comment /* a closed /* simple comment */ is a valid comment. That comment is unfortynately unclosed in the Nested style; it requires an extra closing comment tag to become valid. In Nested mode, the comment /* a closed /* nested */ comment */ is a valid comment.

Frama-C parameters.

"frama_c_exe" : string: Name or pathname to Frama-C binary.; When the value equals the empty string, the semantic analyze (performed by Frama-C) is skipped as well as the C and ML exports required for that analyze. That means that the tool frama-plc-checker.exe does not take in consideration the options -c, --fc, --analyse and --json2 in such a case.

"frama_c_kernel" : string: Options dedicated to Frama-C kernel .

"frama_c_eva" : string: Options dedicated to the plugin’s Eva of Frama-C detecting possible Run-Time-Errors.

"frama_c_wp" : string: Options dedicated to the plugin’s WP of Frama-C dispatching proofs to external provers.

Overloaded parameters.

"frama_plc_share_dir" : string: Path to Frama-PLC resources.; This parameter is mandatory and set by the Windows Batch script (scripts/run-frama-plc-script.bat) viaFRAMA_PLC_SHARE` environment variable.

"dst-dir" : string: Path to the directory used for the issued result files.; Defaults to "", but notices that the Unix script (scripts/frama-plc-script.sh) always overloads this parameter from the value FRAMA_PLC_DESTDIR environment variable. When this variable is unset, the script sets it from the directory name that contents the application file.

These parameters are hidden by the front-ends, since they are overloaded by the Windows Batch or Unix Bash scripts.

4. Declassification

BNF grammar of declassification files:

declassification	:	`'['` rules? `']'`
rules	:	rule ( `','` rule )*
rule	:	`'{' "rule" ':'` rule-name
		`',' "alarms" ':' '['` alarm-patterns? `']'`
		`',' "ctx" ':' '['` ctx-patterns? `']' '}'`
alarm-patterns	:	alarm-pattern ( `','` alarm-pattern )*
alarm-pattern	:	`'['` alarm-kind `','` alarm-value ‘]’
ctx-patterns	:	ctx-pattern ( `','` ctx-pattern )*
ctx-pattern	:	`'['` ctx-kind `','` ctx-value ‘]’

note: the `"filters_out" parameter of the configuration file contents a list of string that can be either the name a declassification file or an identifier (following the syntax of an alarm-kind) related to the kind of alarms to declassify.

All reported checks by Frama-PLC checker that match a rule is declassified. The rule-name is any string for a free use; and can be considered as a user’s comment. To match a rule, the reported checks must match both the alarms and the ctx records. An empty list for theses records gives no constraint.

For example, the following rule absorbs all other rules since it declassifies all reported checks:

{ "rule": "declassifies every things", "alarms": [], "ctx": [] }

The alarms record looks at the category the reported checks. It contents a list alarm-patterns corresponding to a dis-junction of basic alarm-pattern.

Syntax of basic alarm-kind:

"Consecutive_coilRS" or "Consecutive set/reset coils": related to E8.2 - Inadequate logics.

"Constant_expression" or "Expression that has always the same value": related to E4.1 - Constant expressions.

"Constant_section_activation" or "Section activation variable that has always the same value": related to E4.2

"Constant_transition" or "Transition that has always the same value": related to E4.3 - Constant expressions.

"Far_coilRS" or "Non consecutive set/reset coils": related to E8.2 - Inadequate logics.

"Faraway_coilRS" or "Faraway set/reset coils": related to E8.2 - Inadequate logics.

"Fast_outputs_Mast_inputs" or "Fast outputs are read by Mast sections": related to E4.6 - Inadequate interfaces.

"Inadequate_type_edge_detection" or "Rising and falling edge detections on non-EBOOL variables": related to E2.2 - Inadequate types.

"Inadequate_type_eq_neq_of_float_or_duration" or "Equalities and inequalities between durations or reals": related to E2.1 - Inadequate types.

"Jump_backward" or "Backward jumps": related to E8.1 - Inadequate logics.

"Jump_forward" or "Forward jumps": related to E8.1 - Inadequate logics.

"Jump_missing" or "Labels without jump": related to E8.1 - Inadequate logics.

"Jump_undefined" or "Jumps to undefined label": related to E8.1 - Inadequate logics.

"Log_message" or "Log messages": related to E0.1 - Information.

"Loop_stmt" or "Use of loop statements": related to E9.1 - Loop constructs.

"Mast_Fast_common_inputs" or "Mast and Fast sections have common inputs": related to E4.4 - Inadequate interfaces.

"Mast_Fast_common_outputs" or "Mast and Fast sections have common outputs": related to E4.5 - Inadequate interfaces.

"Mast_outputs_Fast_inputs" or "Mast outputs are read by Fast sections": related to E4.7 - Inadequate interfaces.

"Missing_initialized_input" or "Missing inputs having their own initialization": related to E5.2 - Inadequate interfaces.

"Missing_entity" or "Missing entity names": related to E12.1 - Naming Rules.

"Missing_coilRS" or "Only set/reset coils": related to E8.2 - Inadequate logics.

"Missing_comments" or "Uncommented": related to E11.1 - Coding Rules.

"Missing_uninitialized_input" or `“Missing uninitialized inputs”: related to E5.1 - Inadequate interfaces.

"Multiple_wr" or `“Multiple writing”: related to E5.9 - Inadequate interfaces.

"Naming_rule_entity" or "Entity names": related to E12.1 - Naming Rules.

"Naming_rule_external_function" or "External function names": related to E12.6 - Naming Rules.

"Naming_rule_global" or "Variable names": related to E12.3 - Naming Rules.

"Naming_rule_instance" or "Instance names": related to E12.4 - Naming Rules.

"Naming_rule_section" or "Section names": related to E12.2 - Naming Rules.

"Naming_rule_subroutine" or "Subroutine names": related to E12.5 - Naming Rules.

"Hazardous_comment_tags" or "Hazardous comment tags": related to E11.4 - Coding Rules.

"Nop" or "Empty statement": related to E11.2 - Coding Rules.

"Other_property" or "Other ACSL properties": related to E13.4 - Various Frama-C Properties.

"Pragma" or "Use of pragma": related to E11.6 - Coding Rules.

"Reserve_variables" or "Incomplete reserve": related to E6.2 - Inadequate variable declarations.

"RTE_property" or "Run-time errors": related to E.13.3 - Various Frama-C Properties.

"Scanning_order" or "Scanning order": related to E11.3 - Coding Rules.

"SFC_property" or "Exclusive aspect of the diverging conditions from a step to OR branches": related to E13.2 - Various Frama-C Properties.

"Statements_into_comments" or "Statements into comments": related to E11.5 - Coding Rules.

"Topological_variables" or "Use of direct variables": related to E6.1 - Inadequate variable declarations.

"Unauthorized_variable_access" or "Variable accesses outside authorized sections": related to E5.8 - *Inadequate interface"

"Unclosed_comments" or "Unclosed comments": related to E11.4 - Coding Rules.

"Unchecked_code_reachability" or "Unchecked code reachability": related to E7.2 - Dead code.

"Unchecked_expression" or "Unchecked constant expression": related to E4.1 - Constant expressions.

"Unchecked_section_activation" or "Unchecked activation coverage": related to E4.2 - Constant expressions.

"Unchecked_step_reachability" or "Unchecked Grafcet step reachability": related to E7.1 - Dead code.

"Unchecked_transition" or "Unchecked transition coverage": related to E4.3 - Constant expressions.

"Unreached" or "Main code never executed": related to E7.2 - Dead code.

"Unreached_step" or "Unreached Grafcet steps": related to E7.1 - Dead code.

"Unreached_part" or "Piece of code never executed": related to E7.3 - Dead code.

"Unused_output" or "Unused outputs": related to E5.3 - Inadequate interfaces.

The syntax accepts two kind of strings. The first one is a string used internally by Frama-PLC checker (for example inside the Json result files), while the second is directly used by the graphical user interface to pretty print reported checks. Both of them can be used to specify declassification rules.

In order to ease the writing of alarm-patterns, the input format accepts an extension allowing to group several alarm-kind in one entry.

Syntax grouping several alarm-kind:

"E<integer>.*": denotes all alarms related to this category: For example "E12.*" allows to declassify alarms related all naming rules.

"E<integer>.<integer>.*": denotes all alarms related to this sub-category: For example "E8.2.*" allows to declassify alarms related to "Consecutive_coilRS", "Far_coilRS", "Faraway_coilRS" or "Missing_coilRS" (consecutive, non consecutive, faraway or missing set/reset coils).

The default configuration sets the "filters_out" parameter to [ "E0.1.*", "Jump_missing", "Missing_initialized_input", "E5.4.*", "E5.5.*", "E5.6.*", "E5.7.*" ] which is similar to select a declassification file containing that text:

[ { "rule": "no matter 1", "alarms": [[ "E0.1.*", null ]], "ctx": [] },

{ "rule": "no matter 2", "alarms": [[ "Jump_missing", null ]], "ctx": [] },

{ "rule": "no matter 3", "alarms": [[ "Missing_initialized_input", null ]], "ctx": [] },

{ "rule": "no matter 4", "alarms": [[ "E5.4.*", null ]], "ctx": [] },

{ "rule": "no matter 5", "alarms": [[ "E5.5.*", null ]], "ctx": [] },

{ "rule": "no matter 6", "alarms": [[ "E5.6.*", null ]], "ctx": [] },

{ "rule": "no matter 7", "alarms": [[ "E5.7.*", null ]], "ctx": [] },

{ "rule": "no matter 8", "alarms": [[ "Constant_expression", null ]], "ctx": [] },

{ "rule": "no matter 9", "alarms": [[ "Unreached_part", null ]], "ctx": [] }

]

It is possible to declassifify some of the alarms of a same group of alarms in specifying their context-patterns and/or their alarm-value.

Syntax of alarm-value:

null: matches any text value;

string: a text value.

For example, the next rule accepts do declassify the use of FOR constructs of the ST language:

[ { "rule": "accepts FOR loops", "alarms": [ "Loop_stmt", "Use of FOR construct" ], "ctx": [] } ]

A non empty ctx record allows to performs a more selective declassification. Here, the list corresponds to a conjunction of ctx-patterns: the reported checks must match all to them to be declassified.

A context pattern is composed of a context category and an optional value. The context categories and values associated to a reported checks are pretty printed by the graphical user interface.

The first part the pattern (the ctx-kind element) is related to the language used to code the analyzed PLC application while the second part (the ctx-value element) is a text specific to the PLC application. For example, the name of a subroutine of the application is a possible context value, and the notion of subroutine is context category.

Syntax of ctx-value:

null: matches any text value;

string: a text value.

For example, the rule

{ "rule": "no matter about any subroutine", "alarms": [ ], "ctx": [ "Subroutine", null ] }

declassifies all reported checks related to any subroutine while the following rule declassifies all reported checks related the subroutine named my_obsolete_sbr:

{ "rule": "no matter about any subroutine", "alarms": [ ], "ctx": [ "Subroutine", "my_obsolete_sbr" ] }

Syntax of ctx-kind:: "acsl-src" or "Property origin"; "acsl-stat" or "ACSL property status"; "alarm" or "Alarm"; "c-func" or "C function"; "c-glob" or "C global"; "call-dfb-obj" or "Call to DFB instance"; "call-ef-obj" or "Call to function"; "call-efb-obj" or "Call to EFB instance"; "call-sbr" or "Call to subroutine"; "coil" or "Coil"; "coil-hlt" or "Coil halt"; "coil-n" or "Coil edge down"; "coil-p" or "Coil edge up"; "coil-raz" or "Coil reset"; "coil-set" or "Coil set"; "ef" or "Entity"; "dfb-obj" or "DFB type"; "dfb-obj-prg" or "DFB instance"; "ef-obj" or "EF instance"; "efb-obj" or "EFB type"; "efb-obj-prg" or "EFB instance"; "in" or "Input"; "inout" or "InOut"; "lbl" or "Label"; "ld-obj-prg" or "LD instance"; "ld-sect" or "LD section"; "obj-ini" or "Instance initializer"; "out" or "Output"; "pos" or "LD position"; "sbr" or "Subroutine"; "sfc-act" or "SFC action"; "sfc-sect" or "SFC section"; "st-obj-prg" or "ST instance"; "st-sect" or "ST section"; "tr" or "SFC transition"; "undef-sect" or "Undefined section"; "var" or "Variable"; "var-ini" or "Variable initializer"; "xml-tag" or "Xml tag"

As for the alarm-kind, the syntax of the ctx-kind accepts two kind of strings. The first one is a string used internally by Frama-PLC checker (for example into the Json result files), while the second is directly used by the graphical user interface to pretty print reported checks. Both of them can be used to specify declassification rules.