[aorai] use WP cache in 'prove' ptest configuration

src/plugins/aorai/tests/Aorai_test.ml

@@ -29,6 +29,16 @@ module InternalWpShare =
     let file_kind = "wp share directory"
   end)
 
+module WpCache =
+  P.Filepath(
+  struct
+    let option_name = "-aorai-test-wp-cache"
+    let help = "use custom session dir for storing cache"
+    let arg_name = "dir"
+    let existence = Filepath.Must_exist
+    let file_kind = "wp session directory"
+  end)
+
 module ProveAuxSpec =
   P.False(
   struct
@@ -97,7 +107,12 @@ let extend () =
       File.pretty_ast ~prj:aorai_prj ~fmt ();
       close_out chan;
       let selection =
-        State_selection.of_list [ InternalWpShare.self; ProveAuxSpec.self ]
+        List.fold_left
+          (fun selection state ->
+             State_selection.union
+               (State_selection.with_codependencies state) selection)
+          State_selection.empty
+          [ InternalWpShare.self; ProveAuxSpec.self; WpCache.self ]
       in
       Project.copy ~selection my_project;
       Project.set_current my_project;
@@ -115,6 +130,9 @@ let extend () =
         Wp.Wp_parameters.Split.on();
         Wp.Wp_parameters.SplitMax.set 32;
         Wp.Wp_parameters.Verbose.set 0;
+        if WpCache.is_set () then
+          Wp.Wp_parameters.Session.set (WpCache.get());
+        Wp.Wp_parameters.Cache.set "update";
         Globals.Functions.iter check_auto_func;
       end else begin
         File.pretty_ast ();

src/plugins/aorai/tests/test_config_prove.in

@@ -3,4 +3,4 @@ PLUGIN: aorai eva,from,scope report wp,rtegen
 COMMENT: Path to the library from the test file
 LIBS: @PTEST_SUITE_DIR@/../Aorai_test
 
-MACRO: PROVE_OPTIONS @AORAI_WP_SHARE@ -aorai-test-prove-aux-spec
+MACRO: PROVE_OPTIONS @AORAI_WP_SHARE@ -aorai-test-wp-cache @PTEST_SUITE_DIR@/../wp-cache -aorai-test-prove-aux-spec

src/plugins/aorai/tests/wp-cache/cache/00dd5a7a3cc432b4df4b013be4b68f13.json

+{ "prover": "Alt-Ergo:2.2.0", "verdict": "valid", "time": 0.0178,
+  "steps": 164 }

src/plugins/aorai/tests/wp-cache/cache/00f24ed21bf3667627af87a7aad2d13e.json

+{ "prover": "Alt-Ergo:2.4.1", "verdict": "failed" }

src/plugins/aorai/tests/wp-cache/cache/035a236965b94d35d953120e59db5dd3.json

+{ "prover": "Alt-Ergo:2.2.0", "verdict": "valid", "time": 0.0095,
+  "steps": 46 }

src/plugins/aorai/tests/wp-cache/cache/03dbc70a990032105f7c6d5350d17295.json

+{ "prover": "Alt-Ergo:2.4.1", "verdict": "failed" }

src/plugins/aorai/tests/wp-cache/cache/04499ab5e25024a2d32de361c812e41a.json

+{ "prover": "Alt-Ergo:2.2.0", "verdict": "valid", "time": 0.1532,
+  "steps": 68 }

src/plugins/aorai/tests/wp-cache/cache/04736848b6c66f22bd29c4e629cd41f7.json

+{ "prover": "Alt-Ergo:2.2.0", "verdict": "valid", "time": 0.005,
+  "steps": 46 }

src/plugins/aorai/tests/wp-cache/cache/051a5ac44372692d1b3409d8ee21bc60.json

+{ "prover": "Alt-Ergo:2.2.0", "verdict": "valid", "time": 0.0042,
+  "steps": 22 }

src/plugins/aorai/tests/wp-cache/cache/054da1e7390cb63f96c8e49a4cda6c90.json

+{ "prover": "Alt-Ergo:2.4.1", "verdict": "failed" }

src/plugins/aorai/tests/wp-cache/cache/055509ceb46959b31a289021153bf660.json

+{ "prover": "Alt-Ergo:2.2.0", "verdict": "valid", "time": 0.017,
+  "steps": 161 }

src/plugins/aorai/tests/wp-cache/cache/058e3001d92ae06de3118373ea32e774.json

+{ "prover": "Alt-Ergo:2.4.1", "verdict": "failed" }

src/plugins/aorai/tests/wp-cache/cache/05da49ed09c4a3bb59cc590bd50fa7d2.json

+{ "prover": "Alt-Ergo:2.2.0", "verdict": "valid", "time": 0.0081,
+  "steps": 51 }

src/plugins/aorai/tests/wp-cache/cache/07458184b7679110821cb4b2d643a9bb.json

+{ "prover": "Alt-Ergo:2.4.1", "verdict": "failed" }

src/plugins/aorai/tests/wp-cache/cache/07ecc37a49bc085c637afefafe5d6422.json

+{ "prover": "Alt-Ergo:2.4.1", "verdict": "failed" }

src/plugins/aorai/tests/wp-cache/cache/0802e3e919dbe43c9d16e4cb2f549613.json

+{ "prover": "Alt-Ergo:2.4.1", "verdict": "failed" }

src/plugins/aorai/tests/wp-cache/cache/08f56d36d378d6573464516b5d1041e8.json

+{ "prover": "Alt-Ergo:2.4.1", "verdict": "failed" }

src/plugins/aorai/tests/wp-cache/cache/0acd1e4658f68126cf0aea6cc469febb.json

+{ "prover": "Alt-Ergo:2.4.1", "verdict": "failed" }

src/plugins/aorai/tests/wp-cache/cache/0b6ef7b0d55e2a348f77d14117d9009e.json

+{ "prover": "Alt-Ergo:2.2.0", "verdict": "valid", "time": 0.0237,
+  "steps": 257 }

src/plugins/aorai/tests/wp-cache/cache/0bacc494499b6aa02686d67275f4e8aa.json

+{ "prover": "Alt-Ergo:2.4.1", "verdict": "failed" }