[WP] adds tests

src/plugins/wp/tests/wp_plugin/nth.i

@@ -3,12 +3,74 @@
 */
 
 /*@
-  axiomatic Nth {
+  axiomatic Def {
+
   logic integer f(integer a);
+  logic integer N;
+  logic integer M;
+  logic \list<integer> S;
+  logic \list<integer> A;
+  logic \list<integer> B;
+  logic \list<integer> C;
+
+  logic \list<integer> empty = \Nil;
+  predicate IsEmpty(\list<integer> s) = s == empty;
+
+  predicate P(\list<integer> s) reads \nothing;
+
+  }
+*/
+
+/*@
+  axiomatic MkRepeat {
+
+  check lemma negative_repeat: ok: P( A *^ 0 ) <==> P( S *^ (-1) ) ;
+  check lemma repeat_nil:      ok: P( A *^ 0 ) <==> P( (S *^ 0) *^ N );
+  check lemma repeat_one:      ok: P( S *^ 1 ) <==> P( S );
+  check lemma repeat_repeated: ok: P( (S *^ ((N&1)) *^ (M&2)) ) <==> P( S *^ ((N&1) * (M&2)) );
+
+  }
+*/
+
+/*@
+  axiomatic Equality {
+
+  check lemma left_shift_repeat1:   ok: ( ((S ^ A ^ B) *^ N) ^ S ^ A ) == (S ^ C)
+                                   <==> ( (    (A ^ B ^ S) *^ N) ^ A ) == (    C);
+  check lemma left_unfold_repeat1:  ok: ( ((S ^ A ^ B) *^ 3) ^ A ^ S ) == (S ^ C)
+                          <==> (  A ^ B ^ ((S ^ A ^ B) *^ 2) ^ A ^ S ) == (    C);
 
-  check lemma concat_repeat_swap:
-    \forall \list<integer> x ;
-      \forall integer k ; ((x *^ k) ^ x) == (x ^ (x *^ k));
+  check lemma right_shift_repeat1:  ko: ( A ^ S ^ ((B ^ A ^ S) *^ N) ) == (C ^ S)
+                                   <==> ( A ^ ((S ^ B ^ A    ) *^ N) ) == (C    );
+  check lemma right_unfold_repeat1: ko: ( S ^ A ^ ((B ^ A ^ S) *^ 3) ) == (C ^ S)
+                            <==> ( S ^ A ^ ((B ^ A ^ S) *^ 2) ^ B ^ A) == (C    );
+
+
+  check lemma left_shift_repeat2:   ok: ( ((S ^ A ^ B) *^ N) ^ S ^ A ^ C) == (S ^ A)
+                                   <==> ( (C ^ S) == S && (N<=0 || (A ^ B ^ S ^ S) == S) );
+  check lemma left_unfold_repeat2:  ok: ( ((S ^ A ^ B) *^ 3) ^         C) == (S ^ A)
+                                   <==> (A ^ A ^ B ^ C ^ S) == A ;
+
+  check lemma right_shift_repeat2:  ko: ( C ^ A ^ S ^ ((B ^ A ^ S) *^ N) ) == (A ^ S)
+                                   <==> ( (C ^ S) == S && (N<=0 || (A ^ B ^ S ^ S) == S) );
+  check lemma right_unfold_repeat2: ko: ( C ^         ((B ^ A ^ S) *^ 3) ) == (A ^ S)
+                                   <==> (A ^ B ^ C ^ S ^ S) == S ;
+
+
+
+
+  }
+*/
+
+/*@
+  axiomatic Nth {
+
+  check lemma nth_repeat_undefined_1: ko: \nth (  [| f(0), f(1), f(2), f(3) |] *^ 3, 12 ) ==  f(0);
+
+  check lemma nth_repeat_1: ok: \nth (  [| f(0), f(1), f(2), f(3) |] *^ 3, 0 ) ==  f(0);
+  check lemma nth_repeat_2: ok: \nth (  [| f(0), f(1), f(2), f(3) |] *^ 3, 11 ) ==  f(3);
+  check lemma nth_repeat_3: ok: \nth ( ([| f(0), f(1), f(2), f(3) |] *^ 3) ^ [| f(12) |] , 12 ) ==  f(12);
+  check lemma nth_repeat_4: ok: \nth ( ([| f(0), f(1), f(2), f(3) |] *^ 3) ^ [| f(12),f(13),f(14)|] ^ S, 13 ) ==  f(13);
 
   lemma access_16_16: ok:
   \forall integer k ; 0 <= k < 16 ==>
@@ -19,12 +81,12 @@
   \forall integer k ; 0 <= k < 4 ==>
     f(k)==\nth([| f(0), f(1), f(2),  f(3) |], k);
 
-  lemma eq_repeat_concat_3: ok:
-    \forall \list<integer> x ; (x *^ 3) == (x ^ x ^ x) ;
+  lemma eq_repeat_concat_3: ok: (S *^ 3) == (S ^ S ^ S) ;
 
   lemma access_repeat_concat_3: ok: lack:
-    \forall \list<integer> x ;
-      \forall integer k ; 0 <= k < 3*\length(x) ==> \nth(x *^ 3, k) == \nth(x ^ x ^ x, k) ;
+      \forall integer k ; 0 <= k < 3*\length(S) ==> \nth(S *^ 3, k) == \nth(S ^ S ^ S, k) ;
 
   }
+
+
 */

src/plugins/wp/tests/wp_plugin/oracle/nth.res.oracle

 # frama-c -wp [...]
 [kernel] Parsing nth.i (no preprocessing)
 [wp] Running WP plugin...
+------------------------------------------------------------
+  Axiomatic 'Equality'
+------------------------------------------------------------
+
+Lemma left_shift_repeat1:
+Prove: let a_0 = (concat L_A L_B L_S) in
+       (L_C=(concat (repeat a_0 L_N) L_A))=
+       (L_C=(concat (repeat a_0 L_N) L_A))
+
+------------------------------------------------------------
+
+Lemma left_shift_repeat2:
+Prove: true
+
+------------------------------------------------------------
+
+Lemma left_unfold_repeat1:
+Prove: let a_0 = (concat L_S L_A L_B) in
+       (L_C=(concat L_A L_B (repeat a_0 2) L_A L_S))=
+       (L_C=(concat L_A L_B (repeat a_0 2) L_A L_S))
+
+------------------------------------------------------------
+
+Lemma left_unfold_repeat2:
+Prove: true
+
+------------------------------------------------------------
+
+Lemma right_shift_repeat1:
+Prove: let a_0 = (concat L_S L_B L_A) in
+       (L_C=(concat L_A (repeat a_0 L_N)))=
+       (L_C=(concat L_A (repeat a_0 L_N)))
+
+------------------------------------------------------------
+
+Lemma right_shift_repeat2:
+Prove: true
+
+------------------------------------------------------------
+
+Lemma right_unfold_repeat1:
+Prove: let a_0 = (concat L_B L_A L_S) in
+       (L_C=(concat L_S L_A (repeat a_0 2) L_B L_A))=
+       (L_C=(concat L_S L_A (repeat a_0 2) L_B L_A))
+
+------------------------------------------------------------
+
+Lemma right_unfold_repeat2:
+Prove: true
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Axiomatic 'MkRepeat'
+------------------------------------------------------------
+
+Lemma negative_repeat:
+Prove: true
+
+------------------------------------------------------------
+
+Lemma repeat_nil:
+Prove: true
+
+------------------------------------------------------------
+
+Lemma repeat_one:
+Prove: true
+
+------------------------------------------------------------
+
+Lemma repeat_repeated:
+Prove: let x_0 = ((land 1 L_N)*(land 2 L_M)) in
+       (P_P (repeat L_S x_0)) <-> (P_P (repeat L_S x_0))
+
+------------------------------------------------------------
 ------------------------------------------------------------
   Axiomatic 'Nth'
 ------------------------------------------------------------
@@ -27,18 +102,41 @@ Prove: (0<=k_0) -> (k_0<=3)
 
 Lemma access_repeat_concat_3:
 Assume: 'eq_repeat_concat_3' 'access_4_4' 'access_16_16'
-Prove: (0<=k_0) -> (k_0<(3*(length x_0)))
-       -> ((nth (concat x_0 x_0 x_0) k_0)=(nth (repeat x_0 3) k_0))
+Prove: (0<=k_0) -> (k_0<(3*(length L_S)))
+       -> ((nth (concat L_S L_S L_S) k_0)=(nth (repeat L_S 3) k_0))
 
 ------------------------------------------------------------
 
-Lemma concat_repeat_swap:
-Prove: (repeat x_0 k_0)=(repeat x_0 k_0)
+Lemma eq_repeat_concat_3:
+Assume: 'access_4_4' 'access_16_16'
+Prove: true
 
 ------------------------------------------------------------
 
-Lemma eq_repeat_concat_3:
-Assume: 'access_4_4' 'access_16_16'
+Lemma nth_repeat_1:
+Prove: true
+
+------------------------------------------------------------
+
+Lemma nth_repeat_2:
+Prove: true
+
+------------------------------------------------------------
+
+Lemma nth_repeat_3:
+Prove: true
+
+------------------------------------------------------------
+
+Lemma nth_repeat_4:
 Prove: true
 
 ------------------------------------------------------------
+
+Lemma nth_repeat_undefined_1:
+Prove: let x_0 = (L_f 0) in
+       (nth
+         (repeat (concat (elt x_0) (elt (L_f 1)) (elt (L_f 2)) (elt (L_f 3)))
+           3) 12)=x_0
+
+------------------------------------------------------------

src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.res.oracle

 # frama-c -wp [...]
 [kernel] Parsing nth.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] 4 goals scheduled
+[wp] 21 goals scheduled
 [wp] [Alt-Ergo] Goal typed_lemma_access_16_16_ok : Valid
 [wp] [Alt-Ergo] Goal typed_lemma_access_4_4_ok : Valid
-[wp] [Alt-Ergo] Goal typed_lemma_access_repeat_concat_3_ok_lack : Unsuccess
+[wp] [Alt-Ergo] Goal typed_lemma_access_repeat_concat_3_ok_lack : Valid
 [wp] [Qed] Goal typed_lemma_eq_repeat_concat_3_ok : Valid
-[wp] Proved goals:    3 / 4
-  Qed:             1 
-  Alt-Ergo:        2  (unsuccess: 1)
+[wp] [Alt-Ergo] Goal typed_check_lemma_left_shift_repeat1_ok : Valid
+[wp] [Qed] Goal typed_check_lemma_left_shift_repeat2_ok : Valid
+[wp] [Alt-Ergo] Goal typed_check_lemma_left_unfold_repeat1_ok : Valid
+[wp] [Qed] Goal typed_check_lemma_left_unfold_repeat2_ok : Valid
+[wp] [Qed] Goal typed_check_lemma_negative_repeat_ok : Valid
+[wp] [Qed] Goal typed_check_lemma_nth_repeat_1_ok : Valid
+[wp] [Qed] Goal typed_check_lemma_nth_repeat_2_ok : Valid
+[wp] [Qed] Goal typed_check_lemma_nth_repeat_3_ok : Valid
+[wp] [Qed] Goal typed_check_lemma_nth_repeat_4_ok : Valid
+[wp] [Alt-Ergo] Goal typed_check_lemma_nth_repeat_undefined_1_ko : Unsuccess
+[wp] [Qed] Goal typed_check_lemma_repeat_nil_ok : Valid
+[wp] [Qed] Goal typed_check_lemma_repeat_one_ok : Valid
+[wp] [Alt-Ergo] Goal typed_check_lemma_repeat_repeated_ok : Valid
+[wp] [Alt-Ergo] Goal typed_check_lemma_right_shift_repeat1_ko : Valid
+[wp] [Qed] Goal typed_check_lemma_right_shift_repeat2_ko : Valid
+[wp] [Alt-Ergo] Goal typed_check_lemma_right_unfold_repeat1_ko : Valid
+[wp] [Qed] Goal typed_check_lemma_right_unfold_repeat2_ko : Valid
+[wp] Proved goals:   20 / 21
+  Qed:            12 
+  Alt-Ergo:        8  (unsuccess: 1)
 ------------------------------------------------------------
  Axiomatics                WP     Alt-Ergo  Total   Success
-  Axiomatic Nth             1        2        4      75.0%
+  Axiomatic Equality        4        4        8       100%
+  Axiomatic MkRepeat        3        1        4       100%
+  Axiomatic Nth             5        3        9      88.9%
 ------------------------------------------------------------