[wp] validating output of all tests

src/plugins/wp/tests/wp/oracle_qualif/sharing.res.oracle

@@ -8,7 +8,8 @@
 [wp] Proved goals:    1 / 1
   Qed:             0 
   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
 f                   -       1 (48..60)       1       100%

src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle

@@ -40,7 +40,8 @@
 [wp] Proved goals:   19 / 27
   Qed:            18 
   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
 empty                1     -                 1       100%

src/plugins/wp/tests/wp/oracle_qualif/wp_behav.0.res.oracle

@@ -55,12 +55,13 @@
 [wp] Proved goals:   32 / 38
   Qed:            30 
   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
 f                    5     -                 5       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_label   2    -                 2       100%
 stmt_contract_assigns   5   -                5       100%

src/plugins/wp/tests/wp/oracle_qualif/wp_behav.1.res.oracle

@@ -18,7 +18,8 @@
 [wp] [Alt-Ergo] Goal typed_stmt_contract_assigns_ko_ensures_qed_ko : Unsuccess
 [wp] Proved goals:    0 / 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
 f                   -      -                 3       0.0%

src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle

@@ -21,7 +21,8 @@
 [wp] Proved goals:   10 / 10
   Qed:             9 
   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
 double_call          1      1 (4..16)        2       100%

src/plugins/wp/tests/wp/oracle_qualif/wp_eqb.res.oracle

@@ -8,8 +8,9 @@
 [wp] Proved goals:    1 / 1
   Qed:             0 
   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
-f                   -       1 (32..44)       1       100%
+f                   -       1 (36..48)       1       100%
 -------------------------------------------------------------

src/plugins/wp/tests/wp/oracle_qualif/wp_strategy.res.oracle

@@ -39,7 +39,8 @@
 [wp] Proved goals:   17 / 25
   Qed:            17 
   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
 bts0513             -      -                 2       0.0%

src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.0.res.oracle

@@ -31,7 +31,8 @@
 [wp] Proved goals:   24 / 24
   Qed:            21 
   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
 Lemma               20      1 (1..8)        21       100%

src/plugins/wp/tests/wp_acsl/oracle_qualif/arith.1.res.oracle

@@ -7,7 +7,8 @@
 [wp] [Alt-Ergo] Goal typed_cast_sgn_usgn_ensures_qed_ko_KO : Unsuccess
 [wp] Proved goals:    0 / 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
 cast_sgn_usgn       -      -                 1       0.0%

src/plugins/wp/tests/wp_acsl/oracle_qualif/assign_array.res.oracle

@@ -10,7 +10,8 @@
 [wp] [Qed] Goal typed_jobG_assigns_normal : Valid
 [wp] Proved goals:    4 / 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
 jobA                 2     -                 2       100%

src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_path.res.oracle

@@ -16,7 +16,8 @@
 [wp] Proved goals:    9 / 9
   Qed:             6 
   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
 job                  6      3 (20..32)       9       100%

src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.0.res.oracle

@@ -24,7 +24,8 @@
 [wp] Proved goals:   17 / 17
   Qed:            12 
   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
 call_assigns_all    12      2 (8..20)       14       100%

src/plugins/wp/tests/wp_acsl/oracle_qualif/assigns_range.1.res.oracle

@@ -12,7 +12,8 @@
 [wp] [Alt-Ergo] Goal typed_call_assigns_t4_assigns_normal : Unsuccess
 [wp] Proved goals:    0 / 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
 call_assigns_t1     -      -                 2       0.0%

src/plugins/wp/tests/wp_acsl/oracle_qualif/axioms.res.oracle

@@ -17,7 +17,8 @@
 [wp] Proved goals:    8 / 10
   Qed:             3 
   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
 f                    3      5 (104..128)    10      80.0%

src/plugins/wp/tests/wp_acsl/oracle_qualif/base_offset.res.oracle

@@ -10,7 +10,8 @@
 [wp] Proved goals:    3 / 3
   Qed:             2 
   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
 f                    2      1 (8..20)        3       100%

src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise.res.oracle

@@ -36,7 +36,8 @@
 [wp] Proved goals:   26 / 29
   Qed:            25 
   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
 band                 8     -                 8       100%

src/plugins/wp/tests/wp_acsl/oracle_qualif/bitwise2.res.oracle

@@ -11,7 +11,8 @@
 [wp] [Qed] Goal typed_job4_ensures : Valid
 [wp] Proved goals:    5 / 5
   Qed:             5
-[wp] Report 'tests/wp_acsl/bitwise2.i.0.report.json'
+[wp] Report in:  'tests/wp_acsl/oracle_qualif/bitwise2.0.report.json'
+[wp] Report out: 'tests/wp_acsl/result_qualif/bitwise2.0.report.json'
 -------------------------------------------------------------
 Functions           WP     Alt-Ergo        Total   Success
 job1                 1     -                 1       100%

src/plugins/wp/tests/wp_acsl/oracle_qualif/block_length.res.oracle

@@ -16,7 +16,8 @@
 [wp] [Qed] Goal typed_f_ensures_Pts1 : Valid
 [wp] Proved goals:   10 / 10
   Qed:            10
-[wp] Report 'tests/wp_acsl/block_length.i.0.report.json'
+[wp] Report in:  'tests/wp_acsl/oracle_qualif/block_length.0.report.json'
+[wp] Report out: 'tests/wp_acsl/result_qualif/block_length.0.report.json'
 -------------------------------------------------------------
 Functions           WP     Alt-Ergo        Total   Success
 f                   10     -                10       100%

src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.0.res.oracle

@@ -9,8 +9,9 @@
 [wp] Proved goals:    3 / 3
   Qed:             0 
   Alt-Ergo:        3
-[wp] Report 'tests/wp_acsl/classify_float.c.0.report.json'
+[wp] Report in:  'tests/wp_acsl/oracle_qualif/classify_float.0.report.json'
+[wp] Report out: 'tests/wp_acsl/result_qualif/classify_float.0.report.json'
 -------------------------------------------------------------
 Axiomatics          WP     Alt-Ergo        Total   Success
-Lemma               -       3 (1..12)        3       100%
+Lemma               -       3 (4..16)        3       100%
 -------------------------------------------------------------

src/plugins/wp/tests/wp_acsl/oracle_qualif/classify_float.1.res.oracle

@@ -9,7 +9,8 @@
 [wp] Proved goals:    3 / 3
   Qed:             0 
   alt-ergo:        3
-[wp] Report 'tests/wp_acsl/classify_float.c.1.report.json'
+[wp] Report in:  'tests/wp_acsl/oracle_qualif/classify_float.1.report.json'
+[wp] Report out: 'tests/wp_acsl/result_qualif/classify_float.1.report.json'
 -------------------------------------------------------------
 Axiomatics          WP     Alt-Ergo        Total   Success
 Lemma               -      -                 3       100%