[wp] Moves a test from kernel to WP

src/plugins/wp/tests/wp_acsl/generalized_checks.i

@@ -64,3 +64,17 @@ int caller(int x)
 {
   return job(x); // CA2 is not proved
 }
+
+void loop () {
+  int j = 0;
+  /*@ check loop invariant false_but_preserved: j == 10;
+      loop assigns i;
+   */
+  for (int i = 0; i< 10; i++);
+  /*@ check implied_by_false_invariant: j == 10; */
+ l: /*@ check invariant \true; */ ;
+  if (j >= 10) goto l1;
+  j++;
+  goto l;
+ l1 : ;
+}

src/plugins/wp/tests/wp_acsl/oracle/generalized_checks.res.oracle

 # frama-c -wp [...]
 [kernel] Parsing tests/wp_acsl/generalized_checks.i (no preprocessing)
 [wp] Running WP plugin...
+[wp] tests/wp_acsl/generalized_checks.i:68: Warning: 
+  Unsupported generalized invariant, use loop invariant instead.
+  Ignored invariant 
+  check invariant \true;
 [wp] Warning: Missing RTE guards
+[wp] tests/wp_acsl/generalized_checks.i:75: Warning: 
+  Missing assigns clause (assigns 'everything' instead)
 ------------------------------------------------------------
   Axiomatic 'Th'
 ------------------------------------------------------------
@@ -136,3 +142,28 @@ Call Result at line 52
 Prove: true.
 
 ------------------------------------------------------------
+------------------------------------------------------------
+  Function loop
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'false_but_preserved' (file tests/wp_acsl/generalized_checks.i, line 70):
+Assume { Type: is_sint32(i). (* Then *) Have: i <= 9. }
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'false_but_preserved' (file tests/wp_acsl/generalized_checks.i, line 70):
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Check 'implied_by_false_invariant' (file tests/wp_acsl/generalized_checks.i, line 74):
+Assume { Type: is_sint32(i). (* Else *) Have: 10 <= i. }
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_acsl/generalized_checks.i, line 71):
+Prove: true.
+
+------------------------------------------------------------

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

 # frama-c -wp -wp-timeout 1 [...]
 [kernel] Parsing tests/wp_acsl/generalized_checks.i (no preprocessing)
 [wp] Running WP plugin...
+[wp] tests/wp_acsl/generalized_checks.i:68: Warning: 
+  Unsupported generalized invariant, use loop invariant instead.
+  Ignored invariant 
+  check invariant \true;
 [wp] Warning: Missing RTE guards
-[wp] 17 goals scheduled
+[wp] tests/wp_acsl/generalized_checks.i:75: Warning: 
+  Missing assigns clause (assigns 'everything' instead)
+[wp] 21 goals scheduled
 [wp] [Alt-Ergo] Goal typed_check_lemma_C_ko : Unsuccess
 [wp] [Alt-Ergo] Goal typed_lemma_L_ko : Unsuccess
 [wp] [Alt-Ergo] Goal typed_job_ensures_B : Valid
@@ -20,9 +26,13 @@
 [wp] [Qed] Goal typed_caller_call_job_requires_A : Valid
 [wp] [Qed] Goal typed_caller_call_job_check_requires_CA1 : Valid
 [wp] [Alt-Ergo] Goal typed_caller_call_job_check_requires_CA2_ko : Unsuccess
-[wp] Proved goals:   11 / 17
-  Qed:             9 
-  Alt-Ergo:        2  (unsuccess: 6)
+[wp] [Alt-Ergo] Goal typed_loop_check_loop_invariant_false_but_preserved_preserved : Unsuccess
+[wp] [Alt-Ergo] Goal typed_loop_check_loop_invariant_false_but_preserved_established : Unsuccess
+[wp] [Alt-Ergo] Goal typed_loop_check_implied_by_false_invariant : Unsuccess
+[wp] [Qed] Goal typed_loop_loop_assigns : Valid
+[wp] Proved goals:   12 / 21
+  Qed:            10 
+  Alt-Ergo:        2  (unsuccess: 9)
 ------------------------------------------------------------
  Axiomatics                WP     Alt-Ergo  Total   Success
   Axiomatic Th              -        -        2       0.0%
@@ -30,4 +40,5 @@
  Functions                 WP     Alt-Ergo  Total   Success
   job                       3        2        6      83.3%
   caller                    6        -        9      66.7%
+  loop                      1        -        4      25.0%
 ------------------------------------------------------------

tests/spec/generalized_check.i

 /* run.config
-OPT: -wp -wp-prover qed -wp-msg-key shell -wp-warn-key pedantic-assigns=inactive
 OPT: -eva -eva-use-spec f
 OPT: -print
 */
+
 /*@ check lemma easy_proof: \false; */ // should not be put in any environment
 
 /*@ check requires f_valid_x: \valid(x);

tests/spec/oracle/generalized_check.0.res.oracle

-# frama-c -wp [...]
 [kernel] Parsing tests/spec/generalized_check.i (no preprocessing)
-[wp] Running WP plugin...
-[wp] tests/spec/generalized_check.i:30: Warning: 
-  Unsupported generalized invariant, use loop invariant instead.
-  Ignored invariant 
-  check invariant \true;
-[wp] Warning: Missing RTE guards
-[wp] tests/spec/generalized_check.i:37: Warning: 
-  Missing assigns clause (assigns 'everything' instead)
-[wp] 11 goals scheduled
-[wp] [Qed] Goal typed_f_assigns : Valid
-[wp] [Failed] Goal typed_f_check_f_valid_ko
-[wp] [Qed] Goal typed_f_check_ensures_f_init_x : Valid
-[wp] [Failed] Goal typed_check_lemma_easy_proof
-[wp] [Qed] Goal typed_loop_loop_assigns : Valid
-[wp] [Failed] Goal typed_loop_check_implied_by_false_invariant
-[wp] [Failed] Goal typed_loop_check_loop_invariant_false_but_preserved_established
-[wp] [Failed] Goal typed_loop_check_loop_invariant_false_but_preserved_preserved
-[wp] [Failed] Goal typed_main_call_f_check_requires_f_valid_x
-[wp] [Failed] Goal typed_main_check_main_p_content_ko
-[wp] [Failed] Goal typed_main_check_main_valid_ko
-[wp] Proved goals:    3 / 11
-  Qed:             3
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva:initial-state] Values of globals at initialization
+  
+[eva:alarm] tests/spec/generalized_check.i:23: Warning: 
+  accessing uninitialized left-value. assert \initialized(&c);
+[eva] using specification for function f
+[eva:alarm] tests/spec/generalized_check.i:24: Warning: 
+  function f: precondition 'f_valid_x' got status unknown.
+[eva] tests/spec/generalized_check.i:9: Warning: 
+  no \from part for clause 'assigns *x;'
+[eva:alarm] tests/spec/generalized_check.i:25: Warning: 
+  check 'main_valid_ko' got status unknown.
+[eva:alarm] tests/spec/generalized_check.i:26: Warning: 
+  check 'main_p_content_ko' got status unknown.
+[eva:alarm] tests/spec/generalized_check.i:32: Warning: 
+  loop invariant 'false_but_preserved' got status invalid.
+[eva] tests/spec/generalized_check.i:35: starting to merge loop iterations
+[eva:alarm] tests/spec/generalized_check.i:36: Warning: 
+  check 'implied_by_false_invariant' got status invalid.
+[eva] done for function main
+[eva] ====== VALUES COMPUTED ======
+[eva:final-states] Values at end of function loop:
+  j ∈ {10}
+[eva:final-states] Values at end of function main:
+  a ∈ [--..--]
+  p ∈ {{ NULL ; &a }}
+  __retres ∈ {0}
+[eva:summary] ====== ANALYSIS SUMMARY ======
+  ----------------------------------------------------------------------------
+  3 functions analyzed (out of 3): 100% coverage.
+  In these functions, 25 statements reached (out of 28): 89% coverage.
+  ----------------------------------------------------------------------------
+  Some errors and warnings have been raised during the analysis:
+    by the Eva analyzer:      0 errors    1 warning
+    by the Frama-C kernel:    0 errors    0 warnings
+  ----------------------------------------------------------------------------
+  1 alarm generated by the analysis:
+       1 access to uninitialized left-values
+  ----------------------------------------------------------------------------
+  Evaluation of the logical properties reached by the analysis:
+    Assertions        0 valid     2 unknown     2 invalid      4 total
+    Preconditions     0 valid     1 unknown     0 invalid      1 total
+  0% of the logical properties reached have been proven.
+  ----------------------------------------------------------------------------

tests/spec/oracle/generalized_check.1.res.oracle

 [kernel] Parsing tests/spec/generalized_check.i (no preprocessing)
-[eva] Analyzing a complete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
-  
-[eva:alarm] tests/spec/generalized_check.i:23: Warning: 
-  accessing uninitialized left-value. assert \initialized(&c);
-[eva] using specification for function f
-[eva:alarm] tests/spec/generalized_check.i:24: Warning: 
-  function f: precondition 'f_valid_x' got status unknown.
-[eva] tests/spec/generalized_check.i:9: Warning: 
-  no \from part for clause 'assigns *x;'
-[eva:alarm] tests/spec/generalized_check.i:25: Warning: 
-  check 'main_valid_ko' got status unknown.
-[eva:alarm] tests/spec/generalized_check.i:26: Warning: 
-  check 'main_p_content_ko' got status unknown.
-[eva:alarm] tests/spec/generalized_check.i:32: Warning: 
-  loop invariant 'false_but_preserved' got status invalid.
-[eva] tests/spec/generalized_check.i:35: starting to merge loop iterations
-[eva:alarm] tests/spec/generalized_check.i:36: Warning: 
-  check 'implied_by_false_invariant' got status invalid.
-[eva] done for function main
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function loop:
-  j ∈ {10}
-[eva:final-states] Values at end of function main:
-  a ∈ [--..--]
-  p ∈ {{ NULL ; &a }}
-  __retres ∈ {0}
-[eva:summary] ====== ANALYSIS SUMMARY ======
-  ----------------------------------------------------------------------------
-  3 functions analyzed (out of 3): 100% coverage.
-  In these functions, 25 statements reached (out of 28): 89% coverage.
-  ----------------------------------------------------------------------------
-  Some errors and warnings have been raised during the analysis:
-    by the Eva analyzer:      0 errors    1 warning
-    by the Frama-C kernel:    0 errors    0 warnings
-  ----------------------------------------------------------------------------
-  1 alarm generated by the analysis:
-       1 access to uninitialized left-values
-  ----------------------------------------------------------------------------
-  Evaluation of the logical properties reached by the analysis:
-    Assertions        0 valid     2 unknown     2 invalid      4 total
-    Preconditions     0 valid     1 unknown     0 invalid      1 total
-  0% of the logical properties reached have been proven.
-  ----------------------------------------------------------------------------
+/* Generated by Frama-C */
+/*@ check lemma easy_proof: \false;
+ */
+/*@ check requires f_valid_x: \valid(x);
+    check ensures f_init_x: *\old(x) ≡ 0;
+    assigns *x;
+ */
+void f(int *x)
+{
+  /*@ check f_valid_ko: \valid(x); */ ;
+  *x = 0;
+  return;
+}
+
+void loop(void);
+
+int main(void)
+{
+  int __retres;
+  int volatile c;
+  int a = 4;
+  int *p = (int *)0;
+  if (c) p = & a;
+  f(p);
+  /*@ check main_valid_ko: \valid(p); */ ;
+  /*@ check main_p_content_ko: *p ≡ 0; */ ;
+  loop();
+  __retres = 0;
+  return __retres;
+}
+
+void loop(void)
+{
+  int j = 0;
+  {
+    int i = 0;
+    /*@ check loop invariant false_but_preserved: j ≡ 10;
+        loop assigns i; */
+    while (i < 10) i ++;
+  }
+  /*@ check implied_by_false_invariant: j ≡ 10; */ ;
+  l: /*@ check invariant \true; */ ;
+  if (j >= 10) goto l1;
+  j ++;
+  goto l;
+  l1: ;
+  return;
+}
+
+

tests/spec/oracle/generalized_check.2.res.oracle

-[kernel] Parsing tests/spec/generalized_check.i (no preprocessing)
-/* Generated by Frama-C */
-/*@ check lemma easy_proof: \false;
- */
-/*@ check requires f_valid_x: \valid(x);
-    check ensures f_init_x: *\old(x) ≡ 0;
-    assigns *x;
- */
-void f(int *x)
-{
-  /*@ check f_valid_ko: \valid(x); */ ;
-  *x = 0;
-  return;
-}
-
-void loop(void);
-
-int main(void)
-{
-  int __retres;
-  int volatile c;
-  int a = 4;
-  int *p = (int *)0;
-  if (c) p = & a;
-  f(p);
-  /*@ check main_valid_ko: \valid(p); */ ;
-  /*@ check main_p_content_ko: *p ≡ 0; */ ;
-  loop();
-  __retres = 0;
-  return __retres;
-}
-
-void loop(void)
-{
-  int j = 0;
-  {
-    int i = 0;
-    /*@ check loop invariant false_but_preserved: j ≡ 10;
-        loop assigns i; */
-    while (i < 10) i ++;
-  }
-  /*@ check implied_by_false_invariant: j ≡ 10; */ ;
-  l: /*@ check invariant \true; */ ;
-  if (j >= 10) goto l1;
-  j ++;
-  goto l;
-  l1: ;
-  return;
-}
-
-