[wp_strategies] strategies can be used with Frama-C 26, needs doc

README.md

@@ -15,19 +15,20 @@ The easiest is to use [opam](https://opam.ocaml.org/ "Link to opam
 homepage"), the OCaml package manager. We suppose here that opam
 version `2.1` is used.
 
-### 1. Set a (local) `opam` switch using OCaml 4.14.0
+### 1. Set a (local) opam switch using OCaml 4.14.1
+
 ```sh
 opam switch create --no-install . 4.14.1
 ```
 
-You may of course also use a global `opam` switch. Do not forget to
-update your `opam` environment after installing the switch:
+You may of course also use a global opam switch. Do not forget to
+update your opam environment after installing the switch:
 
 ```sh
 eval $(opam env)
 ```
 
-### 2. Install in `opam` switch
+### 2. Install in opam switch
 
 ```sh
 opam install . [--with-test] [--with-doc] --yes
@@ -42,20 +43,23 @@ If you want to generate ACSL specifications and prove them on the
 generated C code, you will need [Frama-C](https://www.frama-c.com
 "Link to Frama-C homepage") and SMT solvers.
 
-First, install Frama-C through `opam` (we are currently using version
-26.0 `Iron` of Frama-C):
+First, install Frama-C through opam (we are currently using version
+26.1 `Iron` of Frama-C):
 
 ```sh
 opam install frama-c
 
 ```
 
+Notice that if you have installed a local Opam switch, Frama-C should
+be installed in this local switch.
+
 The [Alt-Ergo](https://alt-ergo.ocamlpro.com/ "Link to Alt-Ergo
-homepage") is installed with Frama-C. We recommend to also use two
+homepage") is installed with Frama-C. We also recommend to use two
 others SMT solvers:
 
 * [Z3](https://github.com/Z3Prover/z3 "Link to Z3 Github page"), that
-  can be installed through `opam` with `opam install z3` (or through
+  can be installed through opam with `opam install z3` (or through
   your distribution package manager)
 
 * [CVC4](https://cvc4.github.io/ "Link to CVC4 homepage") that can be
@@ -69,6 +73,29 @@ used by Frama-C for deductive verification:
 why3 config detect
 ```
 
+LustreC use custom strategies for the Frama-C WP plugin that must be
+compiled (TODO: add detail here). Go to the `lustrec_wp_strategies`
+directory and execute the following commands:
+
+```sh
+dune build @install
+dune install
+```
+
+When starting Frama-C, you should now see the following message:
+
+```sh
+[lustrec-wp-strategies] LustreC WP strategies available.
+```
+
+You may uninstall the plugin by executing
+
+```sh
+dune uninstall
+```
+
+in the `lustrec_wp_strategies` directory.
+
 ## Usage
 
 To see a summary of options:
@@ -89,22 +116,26 @@ To compile a Lustre file to C with ACSL annotations:
 ```
 lustrec -acsl-spec [-compile_contracts] <file.lus>
 ```
-The flag `-compile_contracts` enables the (experimental) translation of Kind2-like contracts into ACSL contracts.
 
-To prove ACSL assertions:
+The flag `-compile_contracts` enables the (experimental) translation
+of Kind2-like contracts into ACSL contracts.
+
+To prove ACSL assertions (you should have installed the LustreC
+strategies to use the `LustreC:Transitions` and `LustreC:MemoryPacks`
+strategies, see the [corresponding section](#ACSL generation and
+proof)):
 
 ```sh
 frama-c[-gui]\
- -wp                           `# use WP plugin` \
- -wp-model ref,real            `# use ref memory model and ideal floats as reals model` \
- -wp-prover alt-ergo,z3,cvc4   `# use Alt-Ergo, Z3 and CVC4 solvers` \
- -wp-timeout 30                `# set per proof obligation timeout in seconds` \
- -wp-par 16                    `# set the number of jobs` \
- -wp-no-warn-memory-model      `# dismiss various memory model related warnings` \
- -load-module strategy.ml      `# use custom proof strategies selected by names below` \
- -wp-auto LustreC:Transitions,LustreC:MemoryPacks \
- -wp-auto-depth 100            `# set the recursive depth limit of custom strategies use` \
- -wp-auto-width 100            `# set the maxnumber of subgoals for custom strategies use` \
+ -wp                                                `# use WP plugin` \
+ -wp-model ref,real                                 `# use ref memory model and ideal floats as reals model` \
+ -wp-prover alt-ergo,z3,cvc4                        `# use Alt-Ergo, Z3 and CVC4 solvers` \
+ -wp-timeout 30                                     `# set per proof obligation timeout in seconds` \
+ -wp-par 16                                         `# set the number of jobs` \
+ -wp-no-warn-memory-model                           `# dismiss various memory model related warnings` \
+ -wp-auto LustreC:Transitions,LustreC:MemoryPacks   `# use LustreC custom strategies` \
+ -wp-auto-depth 100                                 `# set the recursive depth limit of custom strategies use` \
+ -wp-auto-width 100                                 `# set the maxnumber of subgoals for custom strategies use` \
  <file.c>
 ```
 

lustrec_wp_strategies/dune

+(rule
+ (alias frama-c-configure)
+ (deps (universe))
+ (action (progn
+          (echo "LustreC WP Strategies:" %{lib-available:frama-c-lustrec-wp-strategies.core} "\n")
+          (echo "- Frama-C:" %{lib-available:frama-c.kernel} "\n")
+          (echo "- WP plugin:" %{lib-available:frama-c-wp.core} "\n")))
+)
+
+(library
+ (optional)
+ (name lustrec_wp_strategies)
+ (public_name frama-c-lustrec-wp-strategies.core)
+ (flags -open Frama_c_kernel :standard -w -9)
+ (libraries frama-c.kernel frama-c-wp.core)
+)
+
+(plugin
+ (optional)
+ (name lustrec-wp-strategies)
+ (libraries frama-c-lustrec-wp-strategies.core)
+ (site (frama-c plugins))
+)

lustrec_wp_strategies/dune-project

+(lang dune 3.2)
+(using dune_site 0.1)
+
+(name frama-c-lustrec-wp-strategies)
+(maintainers "Lélio Brun, Christophe Garion, Pierre-Loïc Garoche, Xavier Thirioux")
+
+(package (name frama-c-lustrec-wp-strategies)
+ (depends
+  ("frama-c" (>= 26.1))
+ )
+ (tags ("Frama-C LustreC WP strategies"))
+ (allow_empty)
+)

lustrec_wp_strategies/lustrec_wp_strategies.ml

+(** LustreC WP strategies plug-in.
+
+    No function is exported. *)

strategy.ml → lustrec_wp_strategies/lustrec_wp_strategies_definitions.ml

@@ -270,9 +270,3 @@ class lustrec_memory_packs : Strategy.heuristic =
       | _ ->
         ()
   end
-
-(* Register the strategies *)
-let () =
-  Strategy.register (new lustrec_transitions);
-  (* Strategy.register (new lustrec_reset_cleared); *)
-  Strategy.register (new lustrec_memory_packs)

lustrec_wp_strategies/lustrec_wp_strategies_options.ml

+(* Register the plugin *)
+let help_msg = "WP strategies needed for proving ACSL assertions generating with LustreC"
+
+module Self = Plugin.Register
+  (struct
+    let name = "LustreC WP Strategies"
+    let shortname = "lustrec-wp-strategies"
+    let help = help_msg
+  end)

lustrec_wp_strategies/lustrec_wp_strategies_run.ml

+(* Register strategies and print simple message *)
+let run () =
+  Lustrec_wp_strategies_options.Self.result "LustreC WP strategies available."
+
+let () =
+  Wp.Strategy.register (new Lustrec_wp_strategies_definitions.lustrec_transitions);
+  Wp.Strategy.register (new Lustrec_wp_strategies_definitions.lustrec_memory_packs);
+  Db.Main.extend run