From c28e8897e01136321b06ffbbdd27c286406c603a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 18 May 2020 15:55:03 +0200
Subject: [PATCH] [wp] updated scripts
---
src/plugins/wp/Makefile.in | 54 +++++++++++++------
src/plugins/wp/tests/test_config_qualif | 2 +-
.../init_t2_bis_v2_assigns_exit_part2.json | 4 +-
.../init_t2_bis_v2_assigns_normal_part2.json | 4 +-
.../init_t2_bis_v2_loop_assigns_part2.json | 4 +-
.../init_t2_bis_v2_loop_assigns_part3.json | 4 +-
.../script/init_t2_v2_assigns_part2.json | 4 +-
.../init_t2_v2_loop_assigns_2_part2.json | 4 +-
.../init_t2_v2_loop_assigns_2_part3.json | 4 +-
.../script/init_t2_v2_loop_assigns_part2.json | 4 +-
.../script/init_t2_v2_loop_assigns_part3.json | 4 +-
.../script/init_t2_v3_assigns_part2.json | 4 +-
.../script/init_t2_v3_loop_assigns_part2.json | 4 +-
.../script/init_t2_v3_loop_assigns_part3.json | 4 +-
14 files changed, 62 insertions(+), 42 deletions(-)
diff --git a/src/plugins/wp/Makefile.in b/src/plugins/wp/Makefile.in
index 78a1e1f406a..befdabcf3fc 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 88bdf5005c1..c40c09b1f6a 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 b06ce9ccfcc..81931e7582d 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 b06ce9ccfcc..81931e7582d 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 f9f58898acf..e735dc8ad62 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 fe639edd942..01fc9b21826 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 4b1abcfa72e..6168a773969 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 3040351c102..27f3c51ba83 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 b496d0106fd..60c3f311be2 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 7e4947eb9fa..7297a4bc533 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 605afb5c888..4bad3f08d5e 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 3bc864917bf..6b363edb0f7 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 4f321604a47..957e4cdf739 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 834884c881e..9a022b74ecf 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 } ] } } ]
--
GitLab