[WP] add a test of the introduced rule

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

@@ -124,3 +124,9 @@ void lemma(unsigned a, unsigned b, unsigned k) {
   //@ check           ( a & b & 77 & ((1 << (k & 55))-1) ) == ( (a & b & 77) % (1 << (k & 55)) );
 
 }
+
+//@ ensures \result == (x & 0xFF) ;
+unsigned char cast_uchar(int x) {
+  unsigned char c = x;
+  return c;
+}

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

@@ -218,6 +218,14 @@ Assume {
 }
 Prove: b != a.
 
+------------------------------------------------------------
+------------------------------------------------------------
+  Function cast_uchar
+------------------------------------------------------------
+
+Goal Post-condition (file bitwise.i, line 128) in 'cast_uchar':
+Prove: true.
+
 ------------------------------------------------------------
 ------------------------------------------------------------
   Function lemma

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

@@ -2,7 +2,7 @@
 [kernel] Parsing bitwise.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
-[wp] 37 goals scheduled
+[wp] 38 goals scheduled
 [wp] [Qed] Goal typed_band_ensures : Valid
 [wp] [Qed] Goal typed_band_ensures_band0 : Valid
 [wp] [Qed] Goal typed_band_bit0_ensures_band1 : Valid
@@ -40,8 +40,9 @@
 [wp] [Qed] Goal typed_lemma_check_5 : Valid
 [wp] [Qed] Goal typed_lemma_check_6 : Valid
 [wp] [Qed] Goal typed_lemma_check_7 : Valid
-[wp] Proved goals:   37 / 37
-  Qed:            33 
+[wp] [Qed] Goal typed_cast_uchar_ensures : Valid
+[wp] Proved goals:   38 / 38
+  Qed:            34 
   Alt-Ergo:        4
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
@@ -55,4 +56,5 @@
   band_bool                 1        1        2       100%
   bxor_bool                 1        1        2       100%
   lemma                     7        -        7       100%
+  cast_uchar                1        -        1       100%
 ------------------------------------------------------------