[wp/tests] added option -wp-no-cache-env

FRAMAC_WP_CACHE=update ./ptests.opt src/plugins/wp/tests -config qualif

src/plugins/wp/ProverWhy3.ml

@@ -1216,12 +1216,14 @@ module MODE = WpContext.StaticGenerator(Datatype.Unit)
       let name = "Wp.Cache.mode"
       let compile () =
         try
+          if not (Wp_parameters.CacheEnv.get()) then
+            raise Not_found ;
           let origin = "FRAMAC_WP_CACHE" in
           parse_mode ~origin ~fallback:"-wp-cache" (Sys.getenv origin)
         with Not_found ->
         try
-          parse_mode ~origin:"-wp-cache" ~fallback:"none"
-            (Wp_parameters.Cache.get())
+          let mode = Wp_parameters.Cache.get() in
+          parse_mode ~origin:"-wp-cache" ~fallback:"none" mode
         with Not_found ->
           if Wp_parameters.has_session ()
           then Update else NoCache

src/plugins/wp/tests/wp_acsl/oracle_qualif/boolean.0.session/cache/e6ecc4f1631de0750d8153bb21c50f91.json

+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0158,
+  "steps": 40 }

src/plugins/wp/tests/wp_bts/oracle_qualif/issue_711.0.session/cache/2317c201cc3d414db2797a9b48f01af9.json

+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0139,
+  "steps": 4 }

src/plugins/wp/tests/wp_plugin/nosession.i

@@ -4,7 +4,7 @@
 
 /* run.config_qualif
    CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp-share ./share -wp-msg-key shell
-   OPT: -wp -wp-prover alt-ergo -wp-session shall_not_exists_dir -wp-cache offline
+   OPT: -wp -wp-prover alt-ergo -wp-session shall_not_exists_dir -wp-cache offline -wp-no-cache-env
    COMMENT: The session directory shall not be created
  */
 

src/plugins/wp/tests/wp_plugin/removed.i

 /* run.config_qualif
-   CMD: @frama-c@ -wp-share ./share -wp-msg-key no-cache-info,success-only -wp-par 1 -wp-session @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache offline
+   CMD: @frama-c@ -wp-share ./share -wp-msg-key no-cache-info,success-only -wp-par 1 -wp-session @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache replay
    OPT: -eva -eva-msg-key=-summary -then -wp -then -no-eva -warn-unsigned-overflow -wp
  */
 

src/plugins/wp/wp_parameters.ml

@@ -589,8 +589,15 @@ module Cache = String
          - 'replay': update mode with no cache update\n\
          - 'rebuild': always run provers and update cache\n\
          - 'offline': use cache but never run provers\n\
-         This option is overriden by environment variable FRAMAC_WP_CACHE.\
-        "
+         This option is overriden by environment variable FRAMAC_WP_CACHE,\
+         unless -wp-no-cache-env is used."
+    end)
+
+let () = Parameter_customize.set_group wp_prover
+module CacheEnv = True
+    (struct
+      let option_name = "-wp-cache-env"
+      let help = "Use environment variable FRAMAC_WP_CACHE to override -wp-cache"
     end)
 
 let () = Parameter_customize.set_group wp_prover

src/plugins/wp/wp_parameters.mli

@@ -107,6 +107,7 @@ module Generate:Parameter_sig.Bool
 module Provers: Parameter_sig.String_list
 module RunAllProvers: Parameter_sig.Bool
 module Cache: Parameter_sig.String
+module CacheEnv: Parameter_sig.Bool
 module Drivers: Parameter_sig.String_list
 module Script: Parameter_sig.String
 module UpdateScript: Parameter_sig.Bool