[WP] adds tests

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

@@ -35,6 +35,16 @@
 /*@
   axiomatic Equality {
 
+  check lemma constructor_elt: ok: [| 1 |] != [| 2 |] ;
+
+  check lemma not_nil_elt: ok: ([| 1 |] ^ A) != A ;
+
+
+  check lemma repeat1: ko: (S *^ N) == (S *^ M)
+                      <==> (  N == M || ( ((S *^ N) ^ A) == A && ((S *^ M) ^ A) == A ) ) ;
+
+  check lemma repeat2: ok: ( ((S *^ N) ^ S) *^ M ) == ( ( S ^ (S *^ N)) *^ M ) ;
+
   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)

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

@@ -5,6 +5,11 @@
   Axiomatic 'Equality'
 ------------------------------------------------------------
 
+Lemma constructor_elt:
+Prove: true
+
+------------------------------------------------------------
+
 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))=
@@ -29,6 +34,21 @@ Prove: true
 
 ------------------------------------------------------------
 
+Lemma not_nil_elt:
+Prove: true
+
+------------------------------------------------------------
+
+Lemma repeat1:
+Prove: true
+
+------------------------------------------------------------
+
+Lemma 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)))=

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] 21 goals scheduled
+[wp] 26 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 : Valid
+[wp] [Qed] Goal typed_check_lemma_constructor_elt_ok : Valid
 [wp] [Qed] Goal typed_lemma_eq_repeat_concat_3_ok : Valid
 [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_not_nil_elt_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_repeat1_ko : Valid
+[wp] [Qed] Goal typed_check_lemma_repeat2_ok : Valid
 [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
@@ -23,12 +27,13 @@
 [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 
+[wp] [Qed] Goal typed_check_lemma_subsequence1_ko : Valid
+[wp] Proved goals:   25 / 26
+  Qed:            17 
   Alt-Ergo:        8  (unsuccess: 1)
 ------------------------------------------------------------
  Axiomatics                WP     Alt-Ergo  Total   Success
-  Axiomatic Equality        4        4        8       100%
+  Axiomatic Equality        9        4       13       100%
   Axiomatic MkRepeat        3        1        4       100%
   Axiomatic Nth             5        3        9      88.9%
 ------------------------------------------------------------