Skip to content
Snippets Groups Projects
Commit c28e8897 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp] updated scripts

parent bb5db4c9
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 62 additions and 42 deletions
src/plugins/wp/Makefile.in
+ 37
− 17
View file @ c28e8897
......@@ -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 ---
......
src/plugins/wp/tests/test_config_qualif
+ 1
− 1
View file @ c28e8897
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:
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json
+ 2
− 2
View file @ c28e8897
......@@ -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 } ] } } ]
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json
+ 2
− 2
View file @ c28e8897
......@@ -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 } ] } } ]
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json
+ 2
− 2
View file @ c28e8897
......@@ -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 } ] } } ]
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json
+ 2
− 2
View file @ c28e8897
......@@ -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 } ] } } ]
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_assigns_part2.json
+ 2
− 2
View file @ c28e8897
......@@ -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 } ] } } ]
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part2.json
+ 2
− 2
View file @ c28e8897
......@@ -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 } ] } } ]
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part3.json
+ 2
− 2
View file @ c28e8897
......@@ -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 } ] } } ]
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part2.json
+ 2
− 2
View file @ c28e8897
......@@ -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 } ] } } ]
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part3.json
+ 2
− 2
View file @ c28e8897
......@@ -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 } ] } } ]
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_assigns_part2.json
+ 2
− 2
View file @ c28e8897
......@@ -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 } ] } } ]
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part2.json
+ 2
− 2
View file @ c28e8897
......@@ -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 } ] } } ]
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part3.json
+ 2
− 2
View file @ c28e8897
......@@ -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 } ] } } ]
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment