[aorai] use global wp-cache for caching results

src/plugins/aorai/Makefile.in

@@ -117,6 +117,16 @@ CONFIG_STATUS_DIR=.
 AORAI_WP_SHARE=
 endif
 
+TEST_DEPENDENCIES:= \
+  $(Aorai_DIR)/tests/Aorai_test.cmxs \
+  $(Aorai_DIR)/tests/Aorai_test.cmo \
+  $(Aorai_DIR)/tests/ya/name_projects.cmxs \
+  $(Aorai_DIR)/tests/ya/name_projects.cmo
+
+Aorai_DEFAULT_TESTS: $(TEST_DEPENDENCIES)
+
+# 'prove' ptests config: ensure ACSL and C instrumentation coincide
+
 $(Aorai_DIR)/tests/ptests_config: $(Aorai_DIR)/tests/test_config_prove
 
 $(Aorai_DIR)/tests/test_config_prove: \
@@ -126,7 +136,14 @@ $(Aorai_DIR)/tests/test_config_prove: \
 	$(SED) -e 's!@AORAI_WP_SHARE@!$(AORAI_WP_SHARE)!' $< > $@
 	$(CHMOD_RO) $@
 
-Aorai_DEFAULT_TESTS: $(Aorai_DIR)/tests/Aorai_test.cmxs $(Aorai_DIR)/tests/Aorai_test.cmo $(Aorai_DIR)/tests/ya/name_projects.cmxs $(Aorai_DIR)/tests/ya/name_projects.cmo
+AORAI_WP_CACHE?=$(abspath $(Aorai_DIR)/../wp-cache)
+
+.PHONY: aorai-test-prove
+aorai-test-prove: $(TEST_DEPENDENCIES) $(Aorai_DIR)/tests/test_config_prove
+	FRAMAC_WP_CACHE=update \
+	FRAMAC_WP_CACHEDIR=$(AORAI_WP_CACHE) \
+	PTESTS_OPTS="-config prove" \
+	$(MAKE) Aorai_TESTS
 
 # Regenerating the Makefile on need
 

src/plugins/aorai/tests/Aorai_test.ml

@@ -29,16 +29,6 @@ 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
@@ -112,7 +102,7 @@ let extend () =
              State_selection.union
                (State_selection.with_codependencies state) selection)
           State_selection.empty
-          [ InternalWpShare.self; ProveAuxSpec.self; WpCache.self ]
+          [ InternalWpShare.self; ProveAuxSpec.self ]
       in
       Project.copy ~selection my_project;
       Project.set_current my_project;
@@ -130,9 +120,6 @@ 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-wp-cache @PTEST_SUITE_DIR@/../wp-cache -aorai-test-prove-aux-spec
+MACRO: PROVE_OPTIONS @AORAI_WP_SHARE@ -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 }