Skip to content
Snippets Groups Projects
Commit 227c7f17 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 95fa1181 19da8753
No related branches found
No related tags found
No related merge requests found
Showing
with 36 additions and 9 deletions
...@@ -31,7 +31,8 @@ ...@@ -31,7 +31,8 @@
[wp] Proved goals: 24 / 24 [wp] Proved goals: 24 / 24
Qed: 21 Qed: 21
Alt-Ergo: 3 Alt-Ergo: 3
[wp] Report 'tests/wp_acsl/arith.i.0.report.json' [wp] Report in: 'tests/wp_acsl/oracle_qualif/arith.0.report.json'
[wp] Report out: 'tests/wp_acsl/result_qualif/arith.0.report.json'
------------------------------------------------------------- -------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success Axiomatics WP Alt-Ergo Total Success
Lemma 20 1 (1..8) 21 100% Lemma 20 1 (1..8) 21 100%
......
...@@ -7,7 +7,8 @@ ...@@ -7,7 +7,8 @@
[wp] [Alt-Ergo] Goal typed_cast_sgn_usgn_ensures_qed_ko_KO : Unsuccess [wp] [Alt-Ergo] Goal typed_cast_sgn_usgn_ensures_qed_ko_KO : Unsuccess
[wp] Proved goals: 0 / 1 [wp] Proved goals: 0 / 1
Alt-Ergo: 0 (unsuccess: 1) Alt-Ergo: 0 (unsuccess: 1)
[wp] Report 'tests/wp_acsl/arith.i.1.report.json' [wp] Report in: 'tests/wp_acsl/oracle_qualif/arith.1.report.json'
[wp] Report out: 'tests/wp_acsl/result_qualif/arith.1.report.json'
------------------------------------------------------------- -------------------------------------------------------------
Functions WP Alt-Ergo Total Success Functions WP Alt-Ergo Total Success
cast_sgn_usgn - - 1 0.0% cast_sgn_usgn - - 1 0.0%
......
{ "wp:global": { "qed": { "total": 4, "valid": 4 },
"wp:main": { "total": 4, "valid": 4 } },
"wp:functions": { "jobA": { "jobA_assigns": { "qed": { "total": 2,
"valid": 2 },
"wp:main": { "total": 2,
"valid": 2 } },
"wp:section": { "qed": { "total": 2,
"valid": 2 },
"wp:main": { "total": 2,
"valid": 2 } } },
"jobG": { "jobG_assigns": { "qed": { "total": 2,
"valid": 2 },
"wp:main": { "total": 2,
"valid": 2 } },
"wp:section": { "qed": { "total": 2,
"valid": 2 },
"wp:main": { "total": 2,
"valid": 2 } } } } }
...@@ -10,7 +10,8 @@ ...@@ -10,7 +10,8 @@
[wp] [Qed] Goal typed_jobG_assigns_normal : Valid [wp] [Qed] Goal typed_jobG_assigns_normal : Valid
[wp] Proved goals: 4 / 4 [wp] Proved goals: 4 / 4
Qed: 4 Qed: 4
[wp] Report 'tests/wp_acsl/assign_array.i.0.report.json' [wp] Report in: 'tests/wp_acsl/oracle_qualif/assign_array.0.report.json'
[wp] Report out: 'tests/wp_acsl/result_qualif/assign_array.0.report.json'
------------------------------------------------------------- -------------------------------------------------------------
Functions WP Alt-Ergo Total Success Functions WP Alt-Ergo Total Success
jobA 2 - 2 100% jobA 2 - 2 100%
......
...@@ -16,7 +16,8 @@ ...@@ -16,7 +16,8 @@
[wp] Proved goals: 9 / 9 [wp] Proved goals: 9 / 9
Qed: 6 Qed: 6
Alt-Ergo: 3 Alt-Ergo: 3
[wp] Report 'tests/wp_acsl/assigns_path.i.0.report.json' [wp] Report in: 'tests/wp_acsl/oracle_qualif/assigns_path.0.report.json'
[wp] Report out: 'tests/wp_acsl/result_qualif/assigns_path.0.report.json'
------------------------------------------------------------- -------------------------------------------------------------
Functions WP Alt-Ergo Total Success Functions WP Alt-Ergo Total Success
job 6 3 (20..32) 9 100% job 6 3 (20..32) 9 100%
......
...@@ -24,7 +24,8 @@ ...@@ -24,7 +24,8 @@
[wp] Proved goals: 17 / 17 [wp] Proved goals: 17 / 17
Qed: 12 Qed: 12
Alt-Ergo: 5 Alt-Ergo: 5
[wp] Report 'tests/wp_acsl/assigns_range.i.0.report.json' [wp] Report in: 'tests/wp_acsl/oracle_qualif/assigns_range.0.report.json'
[wp] Report out: 'tests/wp_acsl/result_qualif/assigns_range.0.report.json'
------------------------------------------------------------- -------------------------------------------------------------
Functions WP Alt-Ergo Total Success Functions WP Alt-Ergo Total Success
call_assigns_all 12 2 (8..20) 14 100% call_assigns_all 12 2 (8..20) 14 100%
......
...@@ -12,7 +12,8 @@ ...@@ -12,7 +12,8 @@
[wp] [Alt-Ergo] Goal typed_call_assigns_t4_assigns_normal : Unsuccess [wp] [Alt-Ergo] Goal typed_call_assigns_t4_assigns_normal : Unsuccess
[wp] Proved goals: 0 / 6 [wp] Proved goals: 0 / 6
Alt-Ergo: 0 (unsuccess: 6) Alt-Ergo: 0 (unsuccess: 6)
[wp] Report 'tests/wp_acsl/assigns_range.i.1.report.json' [wp] Report in: 'tests/wp_acsl/oracle_qualif/assigns_range.1.report.json'
[wp] Report out: 'tests/wp_acsl/result_qualif/assigns_range.1.report.json'
------------------------------------------------------------- -------------------------------------------------------------
Functions WP Alt-Ergo Total Success Functions WP Alt-Ergo Total Success
call_assigns_t1 - - 2 0.0% call_assigns_t1 - - 2 0.0%
......
...@@ -17,7 +17,8 @@ ...@@ -17,7 +17,8 @@
[wp] Proved goals: 8 / 10 [wp] Proved goals: 8 / 10
Qed: 3 Qed: 3
Alt-Ergo: 5 (unsuccess: 2) Alt-Ergo: 5 (unsuccess: 2)
[wp] Report 'tests/wp_acsl/axioms.i.0.report.json' [wp] Report in: 'tests/wp_acsl/oracle_qualif/axioms.0.report.json'
[wp] Report out: 'tests/wp_acsl/result_qualif/axioms.0.report.json'
------------------------------------------------------------- -------------------------------------------------------------
Functions WP Alt-Ergo Total Success Functions WP Alt-Ergo Total Success
f 3 5 (104..128) 10 80.0% f 3 5 (104..128) 10 80.0%
......
...@@ -10,7 +10,8 @@ ...@@ -10,7 +10,8 @@
[wp] Proved goals: 3 / 3 [wp] Proved goals: 3 / 3
Qed: 2 Qed: 2
Alt-Ergo: 1 Alt-Ergo: 1
[wp] Report 'tests/wp_acsl/base_offset.i.0.report.json' [wp] Report in: 'tests/wp_acsl/oracle_qualif/base_offset.0.report.json'
[wp] Report out: 'tests/wp_acsl/result_qualif/base_offset.0.report.json'
------------------------------------------------------------- -------------------------------------------------------------
Functions WP Alt-Ergo Total Success Functions WP Alt-Ergo Total Success
f 2 1 (8..20) 3 100% f 2 1 (8..20) 3 100%
......
...@@ -36,7 +36,8 @@ ...@@ -36,7 +36,8 @@
[wp] Proved goals: 26 / 29 [wp] Proved goals: 26 / 29
Qed: 25 Qed: 25
Alt-Ergo: 1 (unsuccess: 3) Alt-Ergo: 1 (unsuccess: 3)
[wp] Report 'tests/wp_acsl/bitwise.i.0.report.json' [wp] Report in: 'tests/wp_acsl/oracle_qualif/bitwise.0.report.json'
[wp] Report out: 'tests/wp_acsl/result_qualif/bitwise.0.report.json'
------------------------------------------------------------- -------------------------------------------------------------
Functions WP Alt-Ergo Total Success Functions WP Alt-Ergo Total Success
band 8 - 8 100% band 8 - 8 100%
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment