[doc] minor changes

README.md

@@ -15,23 +15,21 @@ autopilots.
 * [OCaml](https://github.com/ocaml/ocaml) (tested with version 4.13.1)
 * [OCamlbuild](https://github.com/ocaml/ocamlbuild) (tested with version 0.14.1)
 * [xml-light](https://github.com/ncannasse/xml-light) (tested with version 2.4)
-<!-- * [CompCert](https://github.com/AbsInt/CompCert) (tested with version 3.9)
+* [Menhir](http://gitlab.inria.fr/fpottier/menhir) (tested with version 20220210)
+* [Coq-Mathcomp-SSReflect](https://math-comp.github.io) (tested with version 1.15.0)
 
-You can install all dependencies using [OPAM](https://opam.ocaml.org)
+The dependencies can be installed using [OPAM](https://opam.ocaml.org)
 (version 2.0 or later):
 
 ```bash
 opam repo add coq-released https://coq.inria.fr/opam/released
-opam update
-opam install menhir.20211012 coq-compcert.3.9 xml-light
-``` -->
+opam install coq ocamlbuild xml-light menhir coq-mathcomp-ssreflect  
+```
 
-MathComp is required and can be installed using [OPAM](https://opam.ocaml.org)
-(version 2.0 or later):
+To generate the documentation, the package `graphviz` must be installed:
 
 ```bash
-opam repo add coq-released https://coq.inria.fr/opam/released
-opam install coq-mathcomp-ssreflect
+sudo apt install graphviz
 ```
 
 ## Using the Generator
@@ -155,7 +153,8 @@ Currently, the generator as some limitations and known issues:
 * Generalize env8 property.
 * Prove that the `on_enter` and `on_enter` are always executed when
   entering or leaving a block.
-* Generate a new `common_flight_plan.c` file from the modified version of `CommonFP.v`.
+* Generate a new `common_flight_plan.c` file from the modified version of
+  `CommonFP.v`. The Coq file is used to verify the semantics preservation theorem.
 * Add a warning for the exceptions with deroute that can be forbidden.
 * Prove that the errors detection always work for forbidden deroute.
 * Reduce the amount of modifications in the preprocessing:

docs/build.md

@@ -7,7 +7,7 @@ The script `configure` realize several steps:
 - It clones the [Paparazzi](https://github.com/paparazzi/paparazzi) project
 and rename the module `env` into `PPRZEnd to be compatible with CompCert.
 - It clones [CompCert](https://github.com/AbsInt/CompCert), configure it
-  (set to install coqdev and clightgen), apply a patch to supports recent
+  (set to install coqdev and clightgen), apply a patch to support recent
   version of Coq and then built it.
 
 ## Build Process
@@ -16,7 +16,6 @@ and rename the module `env` into `PPRZEnd to be compatible with CompCert.
 folder.
 - Add OCaml configuration file in the `extracted` folder. CompCert will not
 require compcert.ini file to work.
-- CoqMakefile then build and verified all the Coq file and extract the
-  OCaml
-code.
+- CoqMakefile then build and verified all the Coq files and extract the
+  OCaml code.
 - Finally, `ocamlbuild` is used to compile the entire project.

docs/coq-descr-files.md

@@ -3,25 +3,28 @@
 The folder `src` contains all the Coq sources of the generator and the
 proof. The sources are divided into different subfolders:
 
-- `common`: Contains common lemmas mainly about list.
+- `common`: Contains common lemmas mainly about lists.
   - `CommonLemmas.v`: lemmas about Coq list.
-  - `CommonStringLemmas.v`: lemmas about Coq String and convertion functions.
+  - `CommonStringLemmas.v`: lemmas about Coq String and conversion
+  functions.
   - `CommonLemmasNat8.v`: lemmas about nat representable on 8 bits.
-  - `CommonLemmasSSR.v`: lemmas about SSR seq and ssrnat.
+  - `CommonSSRLemmas.v`: lemmas about SSR seq and ssrnat.
 
-- `syntax`: Contains the definitions about basics types and the flight plan.
-  - `BasicsTypes.v`: All basic type definition for the flight plan.
+- `syntax`: Contains the definitions of basic types and the flight
+  plan.
+  - `BasicsTypes.v`: All basic type definitions for the flight plan.
   - `FPNavigationMode.v`: Definitions of the flight plan navigation modes.
   - `FlightPlanGeneric.v`: Common definitions for the flight plan.
   - `FlightPlan.v`: Definition of the Flight Plan Coq structures.
-  - `FlightPlanExtended.v`: Definition of the structure for the flight plan extended.
+  - `FlightPlanExtended.v`: Definition of the structure for the flight
+    plan extended.
   - `FlightPlanSized.v`: Definition of dependent type for a well-sized
     flight plan.
 
 - `semantics`: Contains the definitions of the semantics used for the
   verification.
-  - `FPEnvironmentGeneric.v`: Generic definition for the FP Environments that
-  will be used by the semantics.
+  - `FPEnvironmentGeneric.v`: Generic definition for the FP Environments
+    that the semantics will use.
   - `FPEnvironment.v`: Definition of the FP Environment.
   - `FPEnvironmentExtended.v`: Definition of the FPE Environment.
   - `FPEnvironmentSized.v`: Definition of the FPS Environment and the
@@ -30,66 +33,72 @@ proof. The sources are divided into different subfolders:
   - `FPEnvironmentDef.v`: Module type that regroups the specialisation of
     all environment modules (expect FPE that is specialized in FPS env).
   - `FPNavigationModeSem.v`: Semantics of the navigation mode.
-  - `FPBigStepGeneric.v`: Generic definitions of semantics and forwards
-    simualuation. This file also contains common definitions for the
-    Flight plan semantics of FP and FPE. 
+  - `FPBigStepGeneric.v`: Generic definitions of semantics and
+    bisimulation. This file also contains common definitions for the
+    Flight plan semantics of FP and FPE.
   - `FPBigStep.v`: BigStep semantics of the flight plan.
   - `FPBigStepExtended.v`: BigStep semantics of the extended flight plan.
   - `FPBigStepSized.v`: BigStep semantics for the sized flight plan.
   - `FPBigStepClight.v`: Definition of the Clight step in the flight plan
     context.
   - `FPBigStepDef.v`: Module type that regroups the specialisation of
-    all big step definitons.
+    all big step definitions.
 
 - `generator`: Contains all the functions of the generators.
-  - `TmpVariables.v`: Definition of all the temporary variable used in the
+  - `TmpVariables.v`: Definition of all the temporary variables used in the
   Clight code generated.
   - `ClightGeneration.v`: Basics function for the generation of Clight
-    code. Need the parameter function `create_ident` that generate a unique
-    identifiant for any string. This file defines an axiom that this
-    function is injective.
-  - `FBDerouteAnalysis.v`: Function that generates warning for a wrong
-    usage of the forbidden deroutes.
-  - `FPExtended.v`: Definition of the function that convert the flight plan
-    into the extended version.
+    code. Need the parameter functions `create_ident` and `arbitrary_ident`
+    that generates a unique identifier for any string. This file defines
+    axioms that these functions are injective. The file requires also
+    `string_of_ident` parameter function that translates an ident into a
+    string. This function is used to generate error messages.
+  - `FBDerouteAnalysis.v`: Contain a function that generates warnings for
+     wrong usage of the forbidden deroutes.
+  - `FPExtended.v`: Definition of the function that converts the flight
+    plan into the extended version.
   - `FPSizeVerification.v`: Functions that generate errors if they detect
-    that the blocks are badly numbered or if there is more than 255 blocks or
-    stages.
+    that the blocks are badly numbered or if there are more than 255
+    blocks or stages.
   - `FPNavigationModeGen.v`: Functions for the generation of the code of
-    navigation functions.
+     navigation functions.
   - `GvarsVerification.v`: Declaration and verification that global
-    variables defined by the preproc does not overlap with the reserved
-    variables of the flight plan.
+    variables defined by the preprocessing do not overlap with the
+    reserved variables of the flight plan.
   - `Generator.v`: Functions for the generation of the Clight code from a
     flight plan.
   - `AuxFunctions.v`: Generation of the auxiliary functions such as
     `pre_call_block`, `post_call_block` and `forbidden_deroute`.
 
-- `verification`: Contains the the proof for the verification of the
+- `verification`: Contains the proof for the verification of the
   semantics preservation.
   - `MatchFPwFPE.v`: Definition of matching relation between FP and
     FPE environment.
-  - `MatchFPSwClight.v`: Defintion of the matching relation between FPS and Clight environment.
-  - `ClightLemmas.v`: lemmas about clight properties.
-  - `GeneratorProperties.v`: Properties about the generator needed for the verification.
+  - `MatchFPSwClight.v`: Definition of the matching relation between FPS
+    and Clight environment.
+  - `ClightLemmas.v`: Lemmas about Clight properties.
+  - `GeneratorProperties.v`: Properties about the generator needed for the
+    verification.
   - `CommonFPDefinition.v`: Contains definitions of functions and lemmas
-    refering the CommonFP file generated from the common C code.
+    referring to the CommonFP file generated from the common C code.
   - `CommonFPSimplified.v`: Contains a simplified version of CommonFP (all
     the built-in functions are removed).
   - `ExtractTraceGeneric.v`: Lemmas and properties about the extraction of
     trace in a generic environment.
-  - `ExtractTraceFPEnv.v`: Lemmas and properties about the extraction of trace
-    generated in the fp_env.
+  - `ExtractTraceFPEnv.v`: Lemmas and properties about the extraction of
+    trace generated in the `fp_env`.
   - `CommonFPVerification.v`: Contains the lemmas that execute the Common C
     function using the Clight semantics.
-  - `VerifFPtoFPE.v`: File containing the forward simulation proof between FP
-    and FPE semantics.
-  - `VerifFPEtoFPS.v`: File containing the semantics forward simulation
+  - `FPNavigationModeVerification.v`: Verification of the semantics
+    preservation for the navigation mode.
+  - `VerifFPtoFPE.v`: File containing the bisimulation proof between
+    FP and FPE semantics.
+  - `VerifFPEtoFPS.v`: File containing the semantics bisimulation
     proof between FPE and FPS semantics.
-  - `VerifFPStoC.v`: File containing the forward simulation proof between FPS
-    and C semantics.
+  - `VerifFPStoC.v`: File containing the bisimulation proof between
+    FPS and Clight semantics.
   - `VerifFPtoC.v`: File regrouping all the proof to verify the general
-    forward simulation theorem between FP and C semantics.
+    bisimulation theorem between FP and Clight semantics.
 
 Finally, the file `extraction.v` is the configuration file for the
 extraction of the Coq to Caml code.

docs/generator_modifications.md

 # Modifications of the current generator
 
 The Ocaml code of the previous Flight Plan generator of
-Paparazzi has been extracted in order to run a behavior test. This test
+Paparazzi have been extracted in order to run a behavior test. This test
 consists to run in parallel flight plans that contain functions that print
 some state information (number of steps, stage executed, current block
 id...). The test then verifies that the execution of the code generated
-with the old and new generator produces the same event trace. As the new
+with the old and new generators produces the same event trace. As the new
 generator implements new features, the two generators do not behave
 similarly. In order to have the same trace, the previous generator has been
 slightly modified with the modifications described below:

docs/tests.md

 # Description of All Tests Available
 
-Several tests are implemented in order to verify that the whole generator is working. All the tests can be launched with the command:
+Several tests are implemented in order to verify that the whole
+generator is working. All the tests can be launched with the command:
 
 ```bash
 make tests
@@ -24,7 +25,9 @@ produces the same result as previously.
 make btests
 ```
 
-These tests generate flight plans with the new and the old generator. Then, the C code generated are compilated and simulated. The goal of these tests is to ensure that the two flight plans behaves similarly.
+These tests generate flight plans with the new and the old generator. Then,
+the C code generated is compilated and simulated. The goal of these tests
+is to ensure that the two flight plans behave similarly.
 
 ## New features Test
 
@@ -41,9 +44,9 @@ make bdtests
 ```
 
 Test to build all the paparazzi flight plans available. The file
-`test/build-tests/non-working-fp.txt` contains the list of all the files that
-did not work also with the old generator. If the generator behaves like the
-old, there are no errors displayed.
+`test/build-tests/non-working-fp.txt` contains the list of all the files
+that did not work also with the old generator. If the generator behaves
+like the old one, there are no errors displayed.
 
 ## Error Message Tests
 
@@ -51,7 +54,7 @@ old, there are no errors displayed.
 make etests
 ```
 
-These tests launche the generator with incorrect files and verify that it
+These tests launch the generator with incorrect files and verify that it
 display correct messages.
 
 ## C Light Tests
@@ -61,7 +64,7 @@ make ctests
 ```
 
 Use `clightgen` on the files in `common-c-code` and verify that the result
-produced is the same than the file in the folder `generated`. As the file
+produced is the same as the file in the folder `generated`. As the file
 `CommonFP.v` has been modified for the verification of the generator. A
 patch is applied on the newly generated file before the execution of the
 `diff` command.

docs/tmp_variables.md

 # Temprorary variables added during the generation
 
+- `tmp_nav_block`: temporary variable to get the value of the block index.
+- `tmp_nav_stage`: temporary variable to get the value of the stage index.
 - `tmp_cond`: needed to compute the `&&` for the exception
 - `tmp_RadOfDeg`: needed for the call of the function `RadOfDeg`
 - `tmp_AltitudeMode`: needed for the call of the altitude functions

ocaml-generator/src_paparazzi/module.ml

@@ -355,8 +355,7 @@ let from_module_name = fun name mtype ->
   let settings = List.map (fun s -> { s with Settings.filename = name }) m.settings in
   { m with xml_filename = name; settings }
 
-(** check if a makefile node is compatible with a target and a firmware
- * TODO add 'board' type filter ? *)
+(** check if a makefile node is compatible with a target and a firmware *)
 let check_mk = fun target firmware mk ->
   (mk.firmware = (Some firmware) || mk.firmware = None || firmware = "none") && GC.test_targets target (GC.bool_expr_of_string mk.targets)
 

src/verification/CommonFPVerification.v

@@ -74,7 +74,10 @@ Section FLIGHT_PLAN.
   Definition f := gen_fp_auto_nav fpe.
 
   (** * Section for the execution of abstract C cond *)
-  (** Axioms to represent the evaluation of abstract condition *)
+  (** Axiom that represent the evaluation of abstract condition. The
+      condition is converted into a trace and replaced by a boolean
+      constant. This constant is the result of the evaluation of the
+      condition using evalc function. *)
   Axiom eval_c_code_cond:
     forall code t b,
       EVAL_Def.eval t code = b
@@ -198,7 +201,9 @@ Section FLIGHT_PLAN.
 
   (** Evaluation of a condition from a function call *)
   (** The axiom state that if there is a call of arbitrary C code, then it
-      can be converted into a trace.*)
+      can be converted into a trace and replaced by a boolean constant.
+      This constant is the result of the evaluation of the condition using
+      evalc function.*)
   Axiom exec_arbitrary_fun_call_with_res:
     forall f func params t b,
     EVAL_Def.eval t (gen_fun_call_sem func params) = b