Skip to content
Snippets Groups Projects
Commit 7ca00ea0 authored by Patrick Baudin's avatar Patrick Baudin
Browse files

Merge branch 'feature/wp/log-journal' into 'master' 

[wp] stabilise qualification tests with journal

See merge request frama-c/frama-c!2178
parents 1b8e195f f44d7d1a
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 264 additions and 15 deletions
src/plugins/wp/register.ml
+ 14
− 5
View file @ 7ca00ea0
...@@ -139,13 +139,22 @@ let do_wp_print_for goals = ...@@ -139,13 +139,22 @@ let do_wp_print_for goals =
let do_wp_report () = let do_wp_report () =
begin begin
let rfiles = Wp_parameters.Report.get () in let reports = Wp_parameters.Report.get () in
if rfiles <> [] then let jreport = Wp_parameters.ReportJson.get () in
if reports <> [] || jreport <> "" then
begin begin
let stats = WpReport.fcstat () in let stats = WpReport.fcstat () in
let jfile = Wp_parameters.ReportJson.get () in begin
if jfile <> "" then WpReport.export_json stats jfile ; match Transitioning.String.split_on_char ':' jreport with
List.iter (WpReport.export stats) rfiles ; | [] | [""] -> ()
| [joutput] ->
WpReport.export_json stats ~joutput () ;
| [jinput;joutput] ->
WpReport.export_json stats ~jinput ~joutput () ;
| _ ->
Wp_parameters.error "Invalid format for option -wp-report-json"
end ;
List.iter (WpReport.export stats) reports ;
end ; end ;
if Wp_parameters.MemoryContext.get () then if Wp_parameters.MemoryContext.get () then
wp_warn_memory_context () wp_warn_memory_context ()
......
src/plugins/wp/tests/test_config_qualif
+ 2
− 1
View file @ 7ca00ea0
CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp -wp-par 1 -wp-steps 1500 -wp-timeout 90 -wp-share ./share -wp-msg-key shell,success-only -wp-report-json @PTEST_FILE@.@PTEST_NUMBER@.report.json -wp-report tests/qualif.report -wp-out @PTEST_FILE@.@PTEST_NUMBER@.out @PTEST_FILE@ CMD: @frama-c@ -no-autoload-plugins -load-module wp -wp -wp-par 1 -wp-steps 1500 -wp-timeout 90 -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-out @PTEST_DIR@/result@PTEST_CONFIG@/@PTEST_NAME@.@PTEST_NUMBER@.out @PTEST_FILE@
LOG: @PTEST_NAME@.@PTEST_NUMBER@.report.json
OPT: OPT:
src/plugins/wp/tests/wp/oracle_qualif/sharing.c.0.report.json 0 → 100644
+ 14
− 0
View file @ 7ca00ea0
{ "wp:global": { "alt-ergo": { "total": 1, "valid": 1, "rank": 13 },
"wp:main": { "total": 1, "valid": 1, "rank": 13 } },
"wp:functions": { "f": { "f_ensures": { "alt-ergo": { "total": 1,
"valid": 1,
"rank": 13 },
"wp:main": { "total": 1,
"valid": 1,
"rank": 13 } },
"wp:section": { "alt-ergo": { "total": 1,
"valid": 1,
"rank": 13 },
"wp:main": { "total": 1,
"valid": 1,
"rank": 13 } } } } }
src/plugins/wp/tests/wp/oracle_qualif/sharing.res.oracle
+ 2
− 1
View file @ 7ca00ea0
...@@ -8,7 +8,8 @@ ...@@ -8,7 +8,8 @@
[wp] Proved goals: 1 / 1 [wp] Proved goals: 1 / 1
Qed: 0 Qed: 0
Alt-Ergo: 1 Alt-Ergo: 1
[wp] Report 'tests/wp/sharing.c.0.report.json' [wp] Report in: 'tests/wp/oracle_qualif/sharing.0.report.json'
[wp] Report out: 'tests/wp/result_qualif/sharing.0.report.json'
------------------------------------------------------------- -------------------------------------------------------------
Functions WP Alt-Ergo Total Success Functions WP Alt-Ergo Total Success
f - 1 (48..60) 1 100% f - 1 (48..60) 1 100%
......
src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.i.0.report.json 0 → 100644
+ 204
− 0
View file @ 7ca00ea0
{ "wp:global": { "alt-ergo": { "total": 9, "valid": 1, "unknown": 8,
"rank": 2 },
"qed": { "total": 18, "valid": 18 },
"wp:main": { "total": 27, "valid": 19, "unknown": 8,
"rank": 2 } },
"wp:functions": { "empty": { "empty_assert": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"wp:section": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } } },
"one_assign": { "one_assign_assert": { "qed": { "total": 1,
"valid": 1 },
"wp:main":
{ "total": 1,
"valid": 1 } },
"wp:section": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } } },
"one_if": { "one_if_assert": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"wp:section": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } } },
"some_seq": { "some_seq_assert_2": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"some_seq_assert": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"wp:section": { "qed": { "total": 2,
"valid": 2 },
"wp:main": { "total": 2,
"valid": 2 } } },
"main_ensures_result": { "main_ensures_result_assert":
{ "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"wp:section": { "qed": { "total": 1,
"valid": 1 },
"wp:main":
{ "total": 1,
"valid": 1 } } },
"main": { "main_assert": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"wp:section": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } } },
"not_main": { "not_main_assert_bad": { "alt-ergo":
{ "total": 1,
"unknown": 1 },
"wp:main":
{ "total": 1,
"unknown": 1 } },
"wp:section": { "alt-ergo": { "total": 1,
"unknown": 1 },
"wp:main": { "total": 1,
"unknown": 1 } } },
"main_assigns_global": { "main_assigns_global_assert_bad":
{ "alt-ergo": { "total": 1,
"unknown": 1 },
"wp:main": { "total": 1,
"unknown": 1 } },
"main_assigns_global_assert_2":
{ "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"main_assigns_global_assert":
{ "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"wp:section": { "alt-ergo":
{ "total": 1,
"unknown": 1 },
"qed": { "total": 2,
"valid": 2 },
"wp:main":
{ "total": 3,
"valid": 2,
"unknown": 1 } } },
"zloop": { "zloop_assert_bad": { "alt-ergo": { "total": 1,
"unknown": 1 },
"wp:main": { "total": 1,
"unknown": 1 } },
"zloop_assert_3": { "alt-ergo": { "total": 1,
"unknown": 1 },
"wp:main": { "total": 1,
"unknown": 1 } },
"zloop_assert_2": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"zloop_assert": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"zloop_loop_invariant": { "alt-ergo":
{ "total": 1,
"unknown": 1 },
"qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 2,
"valid": 1,
"unknown": 1 } },
"zloop_ensures": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"wp:section": { "alt-ergo": { "total": 3,
"unknown": 3 },
"qed": { "total": 4,
"valid": 4 },
"wp:main": { "total": 7,
"valid": 4,
"unknown": 3 } } },
"behavior2": { "behavior2_assert": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"wp:section": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } } },
"behavior3": { "behavior3_assert": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"wp:section": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } } },
"behavior4": { "behavior4_assert": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"wp:section": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } } },
"behavior5": { "behavior5_assert_bad": { "alt-ergo":
{ "total": 1,
"unknown": 1 },
"wp:main":
{ "total": 1,
"unknown": 1 } },
"wp:section": { "alt-ergo": { "total": 1,
"unknown": 1 },
"wp:main": { "total": 1,
"unknown": 1 } } },
"if_assert": { "if_assert_assert_missing_return":
{ "alt-ergo": { "total": 1,
"unknown": 1 },
"wp:main": { "total": 1,
"unknown": 1 } },
"if_assert_assert_3": { "qed": { "total": 1,
"valid": 1 },
"wp:main":
{ "total": 1,
"valid": 1 } },
"if_assert_assert_2": { "alt-ergo":
{ "total": 1,
"unknown": 1 },
"wp:main":
{ "total": 1,
"unknown": 1 } },
"if_assert_assert": { "alt-ergo":
{ "total": 1,
"valid": 1,
"rank": 2 },
"wp:main": { "total": 1,
"valid": 1,
"rank": 2 } },
"wp:section": { "alt-ergo": { "total": 3,
"valid": 1,
"unknown": 2,
"rank": 2 },
"qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 4,
"valid": 2,
"unknown": 2,
"rank": 2 } } },
"compare": { "compare_assert": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } },
"wp:section": { "qed": { "total": 1,
"valid": 1 },
"wp:main": { "total": 1,
"valid": 1 } } } } }
src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle
+ 2
− 1
View file @ 7ca00ea0
...@@ -40,7 +40,8 @@ ...@@ -40,7 +40,8 @@
[wp] Proved goals: 19 / 27 [wp] Proved goals: 19 / 27
Qed: 18 Qed: 18
Alt-Ergo: 1 (unsuccess: 8) Alt-Ergo: 1 (unsuccess: 8)
[wp] Report 'tests/wp/stmtcompiler_test.i.0.report.json' [wp] Report in: 'tests/wp/oracle_qualif/stmtcompiler_test.0.report.json'
[wp] Report out: 'tests/wp/result_qualif/stmtcompiler_test.0.report.json'
------------------------------------------------------------- -------------------------------------------------------------
Functions WP Alt-Ergo Total Success Functions WP Alt-Ergo Total Success
empty 1 - 1 100% empty 1 - 1 100%
......
src/plugins/wp/tests/wp/oracle_qualif/wp_behav.0.res.oracle
+ 3
− 2
View file @ 7ca00ea0
...@@ -55,12 +55,13 @@ ...@@ -55,12 +55,13 @@
[wp] Proved goals: 32 / 38 [wp] Proved goals: 32 / 38
Qed: 30 Qed: 30
Alt-Ergo: 2 (unsuccess: 6) Alt-Ergo: 2 (unsuccess: 6)
[wp] Report 'tests/wp/wp_behav.c.0.report.json' [wp] Report in: 'tests/wp/oracle_qualif/wp_behav.0.report.json'
[wp] Report out: 'tests/wp/result_qualif/wp_behav.0.report.json'
------------------------------------------------------------- -------------------------------------------------------------
Functions WP Alt-Ergo Total Success Functions WP Alt-Ergo Total Success
f 5 - 5 100% f 5 - 5 100%
min 4 - 4 100% min 4 - 4 100%
bhv 2 1 (8..20) 3 100% bhv 2 1 (4..16) 3 100%
stmt_contract 3 - 3 100% stmt_contract 3 - 3 100%
stmt_contract_label 2 - 2 100% stmt_contract_label 2 - 2 100%
stmt_contract_assigns 5 - 5 100% stmt_contract_assigns 5 - 5 100%
......
src/plugins/wp/tests/wp/oracle_qualif/wp_behav.1.res.oracle
+ 2
− 1
View file @ 7ca00ea0
...@@ -18,7 +18,8 @@ ...@@ -18,7 +18,8 @@
[wp] [Alt-Ergo] Goal typed_stmt_contract_assigns_ko_ensures_qed_ko : Unsuccess [wp] [Alt-Ergo] Goal typed_stmt_contract_assigns_ko_ensures_qed_ko : Unsuccess
[wp] Proved goals: 0 / 8 [wp] Proved goals: 0 / 8
Alt-Ergo: 0 (unsuccess: 8) Alt-Ergo: 0 (unsuccess: 8)
[wp] Report 'tests/wp/wp_behav.c.1.report.json' [wp] Report in: 'tests/wp/oracle_qualif/wp_behav.1.report.json'
[wp] Report out: 'tests/wp/result_qualif/wp_behav.1.report.json'
------------------------------------------------------------- -------------------------------------------------------------
Functions WP Alt-Ergo Total Success Functions WP Alt-Ergo Total Success
f - - 3 0.0% f - - 3 0.0%
......
src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle
+ 2
− 1
View file @ 7ca00ea0
...@@ -21,7 +21,8 @@ ...@@ -21,7 +21,8 @@
[wp] Proved goals: 10 / 10 [wp] Proved goals: 10 / 10
Qed: 9 Qed: 9
Alt-Ergo: 1 Alt-Ergo: 1
[wp] Report 'tests/wp/wp_call_pre.c.0.report.json' [wp] Report in: 'tests/wp/oracle_qualif/wp_call_pre.0.report.json'
[wp] Report out: 'tests/wp/result_qualif/wp_call_pre.0.report.json'
------------------------------------------------------------- -------------------------------------------------------------
Functions WP Alt-Ergo Total Success Functions WP Alt-Ergo Total Success
double_call 1 1 (4..16) 2 100% double_call 1 1 (4..16) 2 100%
......
src/plugins/wp/tests/wp/oracle_qualif/wp_eqb.0.report.json 0 → 100644
+ 14
− 0
View file @ 7ca00ea0
{ "wp:global": { "alt-ergo": { "total": 1, "valid": 1, "rank": 10 },
"wp:main": { "total": 1, "valid": 1, "rank": 10 } },
"wp:functions": { "f": { "f_ensures": { "alt-ergo": { "total": 1,
"valid": 1,
"rank": 10 },
"wp:main": { "total": 1,
"valid": 1,
"rank": 10 } },
"wp:section": { "alt-ergo": { "total": 1,
"valid": 1,
"rank": 10 },
"wp:main": { "total": 1,
"valid": 1,
"rank": 10 } } } } }
src/plugins/wp/tests/wp/oracle_qualif/wp_eqb.res.oracle
+ 3
− 2
View file @ 7ca00ea0
...@@ -8,8 +8,9 @@ ...@@ -8,8 +8,9 @@
[wp] Proved goals: 1 / 1 [wp] Proved goals: 1 / 1
Qed: 0 Qed: 0
Alt-Ergo: 1 Alt-Ergo: 1
[wp] Report 'tests/wp/wp_eqb.i.0.report.json' [wp] Report in: 'tests/wp/oracle_qualif/wp_eqb.0.report.json'
[wp] Report out: 'tests/wp/result_qualif/wp_eqb.0.report.json'
------------------------------------------------------------- -------------------------------------------------------------
Functions WP Alt-Ergo Total Success Functions WP Alt-Ergo Total Success
f - 1 (32..44) 1 100% f - 1 (36..48) 1 100%
------------------------------------------------------------- -------------------------------------------------------------
src/plugins/wp/tests/wp/oracle_qualif/wp_strategy.res.oracle
+ 2
− 1
View file @ 7ca00ea0
...@@ -39,7 +39,8 @@ ...@@ -39,7 +39,8 @@
[wp] Proved goals: 17 / 25 [wp] Proved goals: 17 / 25
Qed: 17 Qed: 17
Alt-Ergo: 0 (unsuccess: 8) Alt-Ergo: 0 (unsuccess: 8)
[wp] Report 'tests/wp/wp_strategy.c.0.report.json' [wp] Report in: 'tests/wp/oracle_qualif/wp_strategy.0.report.json'
[wp] Report out: 'tests/wp/result_qualif/wp_strategy.0.report.json'
------------------------------------------------------------- -------------------------------------------------------------
Functions WP Alt-Ergo Total Success Functions WP Alt-Ergo Total Success
bts0513 - - 2 0.0% bts0513 - - 2 0.0%
......
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