diff --git a/src/plugins/wp/Makefile.in b/src/plugins/wp/Makefile.in
index 78a1e1f406a9d1c7fbc4130655881c2e4f719d74..befdabcf3fc0161abd0f9da4837cfe18796b063b 100644
--- a/src/plugins/wp/Makefile.in
+++ b/src/plugins/wp/Makefile.in
@@ -134,7 +134,7 @@ PLUGIN_TESTS_DIRS:= \
wp_region
ifeq ($(FRAMAC_INTERNAL),yes)
-Wp_DEFAULT_TESTS: create_share_link
+Wp_DEFAULT_TESTS: create_share_link $(Wp_DIR)/tests/test_config_qualif
endif
# --------------------------------------------------------------------------
@@ -166,30 +166,50 @@ $(Wp_DIR)/Makefile: $(WP_CONFIGURE_MAKEFILE)
.PHONY: wp-qualif wp-qualif-update wp-qualif-cleanup
-wp-qualif: ./bin/toplevel.opt ./bin/ptests.opt $(WP_CACHE_DIR)
- ./bin/ptests.opt src/plugins/wp/tests -config qualif -error-code
+WP_QUALIF_CACHE?=./wpcache
-wp-qualif-update: ./bin/toplevel.opt ./bin/ptests.opt $(WP_CACHE_DIR)
- git -C $(WP_CACHE_DIR) pull --rebase --prune
+wp-qualif: ./bin/toplevel.opt ./bin/ptests.opt $(WP_QUALIF_CACHE)
+ FRAMAC_WP_CACHE=replay \
+ FRAMAC_WP_CACHEDIR=$(WP_QUALIF_CACHE) \
+ ./bin/ptests.opt src/plugins/wp/tests -config qualif -error-code
+
+wp-qualif-update: ./bin/toplevel.opt ./bin/ptests.opt $(WP_QUALIF_CACHE)
+ @echo "[CACHE] pull cache"
+ git -C $(WP_QUALIF_CACHE) pull --rebase --prune
+ @echo "[TESTS] updating wp-qualif"
FRAMAC_WP_CACHE=update \
- ./bin/ptests.opt src/plugins/wp/tests -config qualif -error-code
- git -C $(WP_CACHE_DIR) status -s -b
+ FRAMAC_WP_CACHEDIR=$(WP_QUALIF_CACHE) \
+ ./bin/ptests.opt src/plugins/wp/tests -config qualif -error-code
+ @echo "[CACHE] cache status"
+ git -C $(WP_QUALIF_CACHE) status -s -b -u no
+ @echo "New entries: `git -C $(WP_QUALIF_CACHE) ls-files --others | wc -l`"
wp-qualif-upgrade: ./bin/toplevel.opt ./bin/ptests.opt
- git -C $(WP_CACHE_DIR) pull --rebase --prune
+ @echo "[CACHE] pull cache"
+ git -C $(WP_QUALIF_CACHE) pull --rebase --prune
+ @echo "[TESTS] upgrading wp-qualif (cache & scripts)"
FRAMAC_WP_CACHE=update \
FRAMAC_WP_SCRIPT=update \
- ./bin/ptests.opt src/plugins/wp/tests -config qualif -error-code
+ FRAMAC_WP_CACHEDIR=$(WP_QUALIF_CACHE) \
+ ./bin/ptests.opt src/plugins/wp/tests -config qualif -error-code
+ @echo "[CACHE] cache status"
+ git -C $(WP_QUALIF_CACHE) status -s -b -u no
wp-qualif-push:
- git -C $(WP_CACHE_DIR) add -A
- git -C $(WP_CACHE_DIR) commit -m "[wp] cache updates"
- git -C $(WP_CACHE_DIR) push -f
-
-wp-qualif-cleanup: wp-qualif-update
-
-$(WP_CACHE_DIR):
- git clone "git@git.frama-c.com:frama-c/wp-cache.git" $(WP_CACHE_DIR)
+ @echo "[CACHE] pushing updates"
+ git -C $(WP_QUALIF_CACHE) add -A
+ git -C $(WP_QUALIF_CACHE) commit -m "[wp] cache updates"
+ git -C $(WP_QUALIF_CACHE) push -f
+
+wp-qualif-status:
+ @echo "[CACHE] cache status"
+ git -C $(WP_QUALIF_CACHE) status -s -b -u no
+ @echo "New entries: `git -C $(WP_QUALIF_CACHE) ls-files --others | wc -l`"
+
+$(WP_QUALIF_CACHE):
+ @echo "[CACHE] cloning wp global at $(WP_QUALIF_CACHE)"
+ @echo "Use env. variable WP_QUALIF_CACHE to change its location"
+ @git clone "git@git.frama-c.com:frama-c/wp-cache.git" $(WP_QUALIF_CACHE)
# --------------------------------------------------------------------------
# --- WP API ---
diff --git a/src/plugins/wp/tests/test_config_qualif b/src/plugins/wp/tests/test_config_qualif
index 88bdf5005c1fd3833c619030920d4ff8dafcfa5a..c40c09b1f6ae94a41ea5089968a786826e98233e 100644
--- a/src/plugins/wp/tests/test_config_qualif
+++ b/src/plugins/wp/tests/test_config_qualif
@@ -1,2 +1,2 @@
-CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp -wp-par 1 -wp-share ./share -wp-msg-key shell,success-only -wp-report tests/qualif.report -wp-session @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache replay @PTEST_FILE@ -wp-cache-dir ./cache
+CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp -wp-par 1 -wp-share ./share -wp-msg-key shell,success-only -wp-report tests/qualif.report -wp-session @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session -wp-cache replay @PTEST_FILE@
OPT:
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json
index b06ce9ccfccfc3c3b4f560ee07709f53085d1160..81931e7582daa0c337bd6ca4478e966bcdf73fa0 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json
@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_102) /\\ (i_1<=i_103) /\\ (0<=i_0) /\\ (i_102<=i_0) /\\ (i_103<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0155,
+ "verdict": "valid", "time": 0.0157,
"steps": 12 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0174,
+ "verdict": "valid", "time": 0.0179,
"steps": 16 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json
index b06ce9ccfccfc3c3b4f560ee07709f53085d1160..81931e7582daa0c337bd6ca4478e966bcdf73fa0 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json
@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_102) /\\ (i_1<=i_103) /\\ (0<=i_0) /\\ (i_102<=i_0) /\\ (i_103<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0155,
+ "verdict": "valid", "time": 0.0157,
"steps": 12 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0174,
+ "verdict": "valid", "time": 0.0179,
"steps": 16 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json
index f9f58898acf9f07e98f3a03aff1b790e5c690741..e735dc8ad622ef9cd78d3503928a9ebe10f429f1 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json
@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_9) /\\ (i_1<=i_10) /\\ (0<=i_0) /\\ (i_9<=i_0) /\\ (i_10<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0178,
+ "verdict": "valid", "time": 0.0179,
"steps": 22 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0245,
+ "verdict": "valid", "time": 0.0193,
"steps": 28 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json
index fe639edd942e0c3a10fa2056e36425592236cc6b..01fc9b218260eca048554e61815331fd305bd82e 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json
@@ -3,8 +3,8 @@
"target": "exists i_1,i_2:int.\n(i_1<=i_0) /\\ (i_2<=i_3) /\\ (0<=i_1) /\\ (i_0<=i_1) /\\ (i_3<=i_2) /\\ (i_1<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0182,
+ "verdict": "valid", "time": 0.0209,
"steps": 16 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0193,
+ "verdict": "valid", "time": 0.0192,
"steps": 22 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_assigns_part2.json
index 4b1abcfa72e2db68b3a7f96e61ba93859a3d6233..6168a77396917172956d78549bbe7dcf3219cf4d 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_assigns_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_assigns_part2.json
@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_156) /\\ (i_1<=i_157) /\\ (0<=i_0) /\\ (i_156<=i_0) /\\ (i_157<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0092,
+ "verdict": "valid", "time": 0.0076,
"steps": 9 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0088,
+ "verdict": "valid", "time": 0.0091,
"steps": 11 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part2.json
index 3040351c102900c9348599dfb2a43b415a279165..27f3c51ba83312b37f018ed69fc8d5b75b527624 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part2.json
@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_13) /\\ (i_1<=i_14) /\\ (0<=i_0) /\\ (i_13<=i_0) /\\ (i_14<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.015,
+ "verdict": "valid", "time": 0.017,
"steps": 22 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0159,
+ "verdict": "valid", "time": 0.0162,
"steps": 24 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part3.json
index b496d0106fd7ee49bdfc3adad4c6a25b1bf781d1..60c3f311be2351c5b45237a512d006907d24cdb1 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part3.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part3.json
@@ -3,8 +3,8 @@
"target": "exists i_0,i_2:int.\n(i_0<=i_1) /\\ (0<=i_0) /\\ (i_1<=i_0) /\\ (j_0<=i_2) /\\ (i_2<=j_0) /\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i0#1$i#1$j#0" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0123,
+ "verdict": "valid", "time": 0.0105,
"steps": 14 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.015,
+ "verdict": "valid", "time": 0.0145,
"steps": 16 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part2.json
index 7e4947eb9fac8add68c3622a0dc8aa4c526a536f..7297a4bc53302546af749a5462ef046aa7bfd5d5 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part2.json
@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_21) /\\ (i_1<=i_22) /\\ (0<=i_0) /\\ (i_21<=i_0) /\\ (i_22<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0151,
+ "verdict": "valid", "time": 0.0163,
"steps": 18 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0146,
+ "verdict": "valid", "time": 0.0156,
"steps": 20 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part3.json
index 605afb5c888573559942ecb623400b58689df42c..4bad3f08d5e99af184014fde5dcee4bb5b90c96b 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part3.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part3.json
@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_8) /\\ (i_1<=i_9) /\\ (0<=i_0) /\\ (i_8<=i_0) /\\ (i_9<=i_1) /\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0151,
+ "verdict": "valid", "time": 0.0163,
"steps": 18 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0146,
+ "verdict": "valid", "time": 0.0156,
"steps": 20 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_assigns_part2.json
index 3bc864917bf2cb48e2475c2b08e15558d696f5df..6b363edb0f779b2bde6f0df63a6319ee68cc03c8 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_assigns_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_assigns_part2.json
@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_148) /\\ (i_1<=i_149) /\\ (0<=i_0) /\\ (i_148<=i_0) /\\ (i_149<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0092,
+ "verdict": "valid", "time": 0.0076,
"steps": 9 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0088,
+ "verdict": "valid", "time": 0.0091,
"steps": 11 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part2.json
index 4f321604a47aeb3d9ba5e1ae23c5598f2eb611f4..957e4cdf73998a9b788068ebfe746895109ec89a 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part2.json
@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_13) /\\ (i_1<=i_14) /\\ (0<=i_0) /\\ (i_13<=i_0) /\\ (i_14<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0138,
+ "verdict": "valid", "time": 0.0152,
"steps": 23 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.014,
+ "verdict": "valid", "time": 0.0165,
"steps": 27 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part3.json
index 834884c881ef2ac497c3466668d1f244ebe89249..9a022b74ecf6f56589717f3faecc6797baf0fb58 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part3.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part3.json
@@ -3,8 +3,8 @@
"target": "exists i_0,i_1:int.\n(i_0<=i_4) /\\ (i_1<=i_6) /\\ (0<=i_0) /\\ (i_4<=i_0) /\\ (i_6<=i_1) /\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
"children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0126,
+ "verdict": "valid", "time": 0.0142,
"steps": 17 } ],
"Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
- "verdict": "valid", "time": 0.0132,
+ "verdict": "valid", "time": 0.014,
"steps": 21 } ] } } ]