Commit 1025038c authored by Andre Maroneze's avatar Andre Maroneze 💬
Browse files

add Frama-PLC plugin page and online manuals

parent 10d2ec8e
Pipeline #45260 passed with stages
in 10 minutes and 45 seconds
......@@ -21,7 +21,7 @@ before_script:
- gem install bundler -v '2.0.2'
- bundle install -j $(nproc) --path vendor
- curl -sL https://deb.nodesource.com/setup_15.x | bash -
- apt-get install -y nodejs
- apt-get install -y nodejs pandoc
- cd generator
- chmod +x ./generate
- curl https://git.frama-c.com/api/v4/projects/780/repository/files/Changelog/raw?ref=master > ../assets/Changelog
......
......@@ -33,3 +33,7 @@ gem 'jekyll-category-pages', group: :jekyll_plugins
gem 'jekyll-minifier', group: :jekyll_plugins
gem "sassc", "< 2.2.0"
gem "webrick", "~> 1.7"
gem "jekyll-pandoc", "~> 2.0"
......@@ -98,6 +98,7 @@ DEPENDENCIES
jekyll-feed (~> 0.12)
jekyll-minifier
jekyll-paginate
jekyll-pandoc (~> 2.0)
minima (~> 2.5)
sassc (< 2.2.0)
tzinfo (~> 1.2)
......
......@@ -57,6 +57,8 @@ collections:
jobs:
output: true
sort_by: posted
online-docs:
output: true
paginate: 5
paginate_path: "/blog/page:num/"
......@@ -65,6 +67,11 @@ category_dir: "/categories/"
category_layout: "blog.html"
permalink: /:year/:month/:day/:title:output_ext
plugins:
- jekyll-pandoc
markdown: Pandoc
# Exclude from processing.
# The following items will not be processed, by default.
# Any item listed under the `exclude:` key here will be automatically added to
......
---
layout: plugin
title: Frama-PLC
description: Analyses of Software Application for Programmable Logic Controllers
key: front
distrib_mode: proprietary
---
## Overview
The Frama-PLC tool performs syntactical and semantic checks of PLC application software (developed with Control Expert by Schneider Electric - tool renamed into EcoStruxure) in relying on Frama-C platform.
The tool is operational and can be considered as an advanced prototype able to analyse ZEF development files (Application exchange files proposed by Schneider Electrics tool).
It supports most of the constructs of the Ladder Diagrams (LD), Sequential Function Charts (SFC) and Structured Text (ST) languages.
## Further Reading
The syntactical checks are reported during the first analysis step of Frama-PLC whereas the semantic checks are reported during the second step what uses EVA and WP plugins of Frama-C.
A viewer tool can be used to navigates into the reported checks and classifies them.
**Online Documentation:**
- [User Manual]({% link _online-docs/frama-plc/frama-plc-user-manual.md %})
- [Check List]({% link _online-docs/frama-plc/frama-plc-check-list.md %})
---
layout: default
css: manual
---
<body class="page nonTouch">
<div id="wrapper" class="hfeed">
{% include headers.html %}
<div id="container" class="mainContainer">
<div class="tabs">
<div class="pageKernel pages">
<div class="wrap">
{{ content }}
</div>
</div>
{% include footer.html %}
<div class="clear"></div>
</div>
</div>
---
layout: manual
markdown: Pandoc
---
# Frama-PLC - Check List #
+------------+------------------------------------------------------------------------------------------------+
| | |
+============+================================================================================================+
| Authors: | P. Baudin and F. Bobot |
+------------+------------------------------------------------------------------------------------------------+
| Institute: | [CEA-List](http://list.cea.fr), Université Paris-Saclay - Software Safety and Security Lab |
+------------+------------------------------------------------------------------------------------------------+
| License: | [Creative Commons Attribution-ShareAlike 4.0 International](https://creativecommons.org/licenses/by-sa/4.0/deed.en) |
+------------+------------------------------------------------------------------------------------------------+
| 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: '\t' 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>:`.
This diff is collapsed.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment