Merge branch 'feature/aorai/use-wp-cache' into 'master'

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

See merge request frama-c/frama-c!3629

nix/default.nix

@@ -253,7 +253,9 @@ pkgs.lib.makeExtensible
           HOME=$(pwd)/home
           why3 config detect
           make src/plugins/aorai/tests/ptests_config
-          make PTESTS_OPTS="-config prove -error-code" Aorai_TESTS
+          export AORAI_WP_CACHE=replay
+          export AORAI_WP_CACHEDIR=${plugins.wp-cache.src}
+          make PTESTS_OPTS="-error-code" aorai-test-prove
         '';
 
         installPhase = ''

src/plugins/aorai/Makefile.in

@@ -117,6 +117,27 @@ 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
+# Launch this configuration for all tests with
+# make aorai-test-prove
+# To launch only one test, you can use PTESTS_OPTS, as in
+# PTESTS_OPTS="tests/ya/stack.i -add-options '-wp-verbose 1'" make aorai-test-prove
+#
+# This requires to have a copy of the wp-cache repository
+# (see ../wp/tests/README.md for more information). If it is not
+# in its default place of ../wp-cache, use AORAI_WP_CACHE variable to give the
+# proper absolute path.
+# Don't forget to add the new cache files to the repo if needed,
+# in particular if CI complains about its aorai-prove target.
+
 $(Aorai_DIR)/tests/ptests_config: $(Aorai_DIR)/tests/test_config_prove
 
 $(Aorai_DIR)/tests/test_config_prove: \
@@ -126,7 +147,15 @@ $(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_CACHEDIR?=$(abspath $(Aorai_DIR)/../wp-cache)
+AORAI_WP_CACHE?=update
+
+.PHONY: aorai-test-prove
+aorai-test-prove: $(TEST_DEPENDENCIES) $(Aorai_DIR)/tests/test_config_prove
+	FRAMAC_WP_CACHE=$(AORAI_WP_CACHE) \
+	FRAMAC_WP_CACHEDIR=$(AORAI_WP_CACHEDIR) \
+	PTESTS_OPTS="$$PTESTS_OPTS -config prove" \
+	$(MAKE) Aorai_TESTS
 
 # Regenerating the Makefile on need
 

src/plugins/aorai/tests/Aorai_test.ml

@@ -97,7 +97,15 @@ 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;
+            Wp.Wp_parameters.CacheEnv.self;
+            Wp.Wp_parameters.Verbose.self;
+          ]
       in
       Project.copy ~selection my_project;
       Project.set_current my_project;
@@ -114,7 +122,8 @@ let extend () =
         Wp.Wp_parameters.Let.off();
         Wp.Wp_parameters.Split.on();
         Wp.Wp_parameters.SplitMax.set 32;
-        Wp.Wp_parameters.Verbose.set 0;
+        if not (Wp.Wp_parameters.Verbose.is_set()) then
+          Wp.Wp_parameters.Verbose.set 0;
         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@ -wp-cache-env -aorai-test-prove-aux-spec