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

[wp/cache] assign a session to each test

parent 2fdb2da3
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 104 additions and 5 deletions
src/plugins/wp/tests/test_config_qualif
+ 1
− 1
View file @ c1ebf079
CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp -wp-par 1 -wp-steps 1500 -wp-timeout 45 -wp-share ./share -wp-msg-key shell,success-only -wp-report-json @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.report.json:@PTEST_DIR@/result@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.report.json -wp-report tests/qualif.report @PTEST_FILE@
CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp -wp-par 1 -wp-steps 1500 -wp-timeout 45 -wp-share ./share -wp-msg-key shell,success-only -wp-report-json @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.report.json:@PTEST_DIR@/result@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.report.json -wp-report tests/qualif.report -wp-session @PTEST_DIR@/oracle@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.session @PTEST_FILE@
LOG: @PTEST_NAME@.@PTEST_NUMBER@.report.json
OPT:
src/plugins/wp/tests/wp_plugin/unsigned.i
+ 1
− 1
View file @ c1ebf079
......@@ -3,7 +3,7 @@
*/
/* run.config_qualif
OPT: -session tests/wp_plugin/unsigned -wp-prover script
OPT: -wp-prover script
*/
/*@
......
src/plugins/wp/tests/wp_tip/tac_split_quantifiers.i
+ 1
− 1
View file @ c1ebf079
......@@ -3,7 +3,7 @@
*/
/* run.config_qualif
OPT: -load-module tests/wp_tip/TacNOP.ml -wp -wp-par 1 -wp-prover script -session tests/wp_tip/tac_split_quantifiers
OPT: -load-module tests/wp_tip/TacNOP.ml -wp -wp-par 1 -wp-prover script
*/
......
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.res.oracle
+ 1
− 2
View file @ c1ebf079
......@@ -10,8 +10,7 @@
[wp] Warning: Missing RTE guards
[wp] 23 goals scheduled
[wp] [Qed] Goal typed_init_t2_bis_v2_loop_assigns_part1 : Valid
[wp] Warning: creating session directory `tests/wp_typed/result_qualif/user_init-session-1'
[wp] Warning: creating session directory `tests/wp_typed/result_qualif/user_init-session-1/wp'
[wp] Warning: creating session directory `tests/wp_typed/oracle_qualif/user_init.1.session'
[wp] [Tactical] Goal typed_init_t2_bis_v2_loop_assigns_part2 : Valid
[wp] [Tactical] Goal typed_init_t2_bis_v2_loop_assigns_part3 : Valid
[wp] [Tactical] Goal typed_init_t2_bis_v2_assigns_exit_part1 : Valid
......
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_bis_v2_assigns_exit_part2.json 0 → 100644
+ 10
− 0
View file @ c1ebf079
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"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": "why3:Alt-Ergo,2.0.0",
"verdict": "valid", "time": 0.0174,
"steps": 12 } ],
"Goal 2/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
"verdict": "valid", "time": 0.0186,
"steps": 16 } ] } } ]
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_bis_v2_assigns_normal_part2.json 0 → 100644
+ 10
− 0
View file @ c1ebf079
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"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": "why3:Alt-Ergo,2.0.0",
"verdict": "valid", "time": 0.0183,
"steps": 12 } ],
"Goal 2/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
"verdict": "valid", "time": 0.0199,
"steps": 16 } ] } } ]
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_bis_v2_loop_assigns_part2.json 0 → 100644
+ 10
− 0
View file @ c1ebf079
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"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": "why3:Alt-Ergo,2.0.0",
"verdict": "valid", "time": 0.0242,
"steps": 22 } ],
"Goal 2/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
"verdict": "valid", "time": 0.0275,
"steps": 28 } ] } } ]
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_bis_v2_loop_assigns_part3.json 0 → 100644
+ 10
− 0
View file @ c1ebf079
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"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": "why3:Alt-Ergo,2.0.0",
"verdict": "valid", "time": 0.0244,
"steps": 16 } ],
"Goal 2/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
"verdict": "valid", "time": 0.0246,
"steps": 22 } ] } } ]
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_assigns_part2.json 0 → 100644
+ 10
− 0
View file @ c1ebf079
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"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": "why3:Alt-Ergo,2.0.0",
"verdict": "valid", "time": 0.0083,
"steps": 9 } ],
"Goal 2/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
"verdict": "valid", "time": 0.0075,
"steps": 11 } ] } } ]
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_loop_assigns_2_part2.json 0 → 100644
+ 10
− 0
View file @ c1ebf079
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"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": "why3:Alt-Ergo,2.0.0",
"verdict": "valid", "time": 0.0113,
"steps": 22 } ],
"Goal 2/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
"verdict": "valid", "time": 0.0127,
"steps": 24 } ] } } ]
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_loop_assigns_2_part3.json 0 → 100644
+ 10
− 0
View file @ c1ebf079
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"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": "why3:Alt-Ergo,2.0.0",
"verdict": "valid", "time": 0.0106,
"steps": 14 } ],
"Goal 2/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
"verdict": "valid", "time": 0.0108,
"steps": 16 } ] } } ]
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_loop_assigns_part2.json 0 → 100644
+ 10
− 0
View file @ c1ebf079
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"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": "why3:Alt-Ergo,2.0.0",
"verdict": "valid", "time": 0.0175,
"steps": 18 } ],
"Goal 2/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
"verdict": "valid", "time": 0.0191,
"steps": 20 } ] } } ]
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v2_loop_assigns_part3.json 0 → 100644
+ 10
− 0
View file @ c1ebf079
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"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": "why3:Alt-Ergo,2.0.0",
"verdict": "valid", "time": 0.0191,
"steps": 18 } ],
"Goal 2/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
"verdict": "valid", "time": 0.021,
"steps": 20 } ] } } ]
src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/typed/typed_init_t2_v3_assigns_part2.json 0 → 100644
+ 10
− 0
View file @ c1ebf079
[ { "header": "Split", "tactic": "Wp.split", "params": {},
"select": { "select": "clause-goal",
"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": "why3:Alt-Ergo,2.0.0",
"verdict": "valid", "time": 0.0055,
"steps": 9 } ],
"Goal 2/2": [ { "prover": "why3:Alt-Ergo,2.0.0",
"verdict": "valid", "time": 0.0068,
"steps": 11 } ] } } ]
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