Merge branch 'fix/wp/null-is-invalid' into 'master'

[wp] Improves null (in)validity

Closes #48

See merge request frama-c/frama-c!2997

src/plugins/wp/Makefile.in

@@ -129,7 +129,7 @@ CEA_WP_GENEREATED= script.ml rformat.ml driver.ml
 # --------------------------------------------------------------------------
 
 PLUGIN_TESTS_DIRS:= \
-  wp wp_plugin wp_acsl wp_bts \
+  why3 wp wp_plugin wp_acsl wp_bts \
   wp_store wp_hoare wp_typed wp_usage \
   wp_gallery wp_manual wp_tip \
   wp_region

src/plugins/wp/MemMemory.ml

@@ -239,27 +239,28 @@ let is_separated args = F.is_true (r_separated args)
 (* --- Simplifier for 'included'                                          --- *)
 (* -------------------------------------------------------------------------- *)
 
-(*
-logic a : int
-logic b : int
+(* See: tests/why3/test_memory.why
+
+   logic a : int
+   logic b : int
 
-predicate R =     p.base = q.base
+   predicate R = p.base = q.base
               /\ (q.offset <= p.offset)
               /\ (p.offset + a <= q.offset + b)
 
-predicate included = 0 < a -> ( 0 <= b and R )
-predicate a_empty = a <= 0
-predicate b_negative = b < 0
+   predicate included = 0 < a -> ( 0 <= b and R )
+   predicate a_empty = a <= 0
+   predicate b_negative = b < 0
 
-lemma SAME_P: p=q -> (R <-> a<=b)
-lemma SAME_A: a=b -> (R <-> p=q)
+   lemma SAME_P: p=q -> (R <-> a<=b)
+   lemma SAME_A: a=b -> (R <-> p=q)
 
-goal INC_P:  p=q -> (included <-> ( 0 < a -> a <= b )) (by SAME_P)
-goal INC_A:  a=b -> 0 < a -> (included <-> R) (by SAME_A)
-goal INC_1:  a_empty -> (included <-> true)
-goal INC_2:  b_negative -> (included <-> a_empty)
-goal INC_3:  not R -> (included <-> a_empty)
-goal INC_4:  not a_empty -> not b_negative -> (included <-> R)
+   goal INC_P:  p=q -> (included <-> ( 0 < a -> a <= b )) (by SAME_P)
+   goal INC_A:  a=b -> 0 < a -> (included <-> R) (by SAME_A)
+   goal INC_1:  a_empty -> (included <-> true)
+   goal INC_2:  b_negative -> (included <-> a_empty)
+   goal INC_3:  not R -> (included <-> a_empty)
+   goal INC_4:  not a_empty -> not b_negative -> (included <-> R)
 *)
 
 let r_included = function
@@ -341,6 +342,32 @@ let phi_addr_of_int p =
     | L.Fun(f,[a]) when f == f_int_of_addr -> a
     | _ -> raise Not_found
 
+(* -------------------------------------------------------------------------- *)
+(* --- Simplifier for (in)validity                                        --- *)
+(* -------------------------------------------------------------------------- *)
+
+let null_base p = e_eq (F.e_fun f_base [p]) F.e_zero
+
+(* See: tests/why3/test_memory.why *)
+
+(* - lemma valid_rd_null: forall m n p. p.base = 0 -> (n <= 0 <-> valid_rd m p n)
+   - lemma valid_rw_null: forall m n p. p.base = 0 -> (n <= 0 <-> valid_rw m p n)
+*)
+let r_valid_unref = function
+  | [_; p; n] when F.decide (null_base p) ->
+      e_leq n e_zero
+  | _ -> raise Not_found
+
+(* - lemma valid_obj_null: forall m n. valid_obj m null n *)
+let r_valid_obj = function
+  | [_; p; _] when F.decide (e_eq p a_null) -> e_true
+  | _ -> raise Not_found
+
+(* - lemma invalid_null: forall m n p. p.base = 0 -> invalid m p n *)
+let r_invalid = function
+  | [_; p; _] when F.decide (null_base p) -> e_true
+  | _ -> raise Not_found
+
 (* -------------------------------------------------------------------------- *)
 (* --- Simplifiers Registration                                           --- *)
 (* -------------------------------------------------------------------------- *)
@@ -358,6 +385,10 @@ let () = Context.register
       F.set_builtin_get f_havoc r_get_havoc ;
       F.set_builtin_1 f_addr_of_int phi_addr_of_int ;
       F.set_builtin_1 f_int_of_addr phi_int_of_addr ;
+      F.set_builtin p_invalid r_invalid ;
+      F.set_builtin p_valid_rd r_valid_unref ;
+      F.set_builtin p_valid_rw r_valid_unref ;
+      F.set_builtin p_valid_obj r_valid_obj ;
     end
 
 (* -------------------------------------------------------------------------- *)

src/plugins/wp/share/why3/frama_c_wp/memory.mlw

@@ -80,7 +80,7 @@ theory Memory
              ( 0 <> p.base /\ 0 <= p.offset /\ p.offset + n <= 1 + m[p.base] ))
 
   predicate invalid (m : map int int) (p:addr) (n:int) =
-    n > 0 -> ( m[p.base] <= p.offset \/ p.offset + n <= 0 )
+    n <= 0 \/ p.base = 0 \/ m[p.base] <= p.offset \/ p.offset + n <= 0
 
   lemma valid_rw_rd :
     forall m : map int int.
@@ -152,7 +152,7 @@ theory Memory
     forall a : int.
     eqmem m1 m2 p a -> eqmem m2 m1 p a
 
-  lemma havoc_access :
+  axiom havoc_access :
     forall m0 m1 : map addr 'a.
     forall q p : addr.
     forall a : int.
@@ -168,7 +168,7 @@ theory Memory
 
   function set_init (m: map addr bool) (p:addr) (a:int) : map addr bool
 
-  lemma set_init_access :
+  axiom set_init_access :
     forall m : map addr bool.
     forall q p : addr.
     forall a : int.

src/plugins/wp/tests/why3/oracle_qualif/spec_memory.res.oracle

+tests/why3/spec_memory.why Spec_memory check_valid_rd: Valid
+tests/why3/spec_memory.why Spec_memory check_valid: Valid
+tests/why3/spec_memory.why Spec_memory invalid_spec: Valid
+tests/why3/spec_memory.why Spec_memory invalid_null_spec: Valid
+tests/why3/spec_memory.why Spec_memory invalid_null: Valid
+tests/why3/spec_memory.why Spec_memory invalid_empty: Valid
+tests/why3/spec_memory.why Spec_memory valid_rd_null: Valid
+tests/why3/spec_memory.why Spec_memory valid_rw_null: Valid
+tests/why3/spec_memory.why Spec_memory valid_obj_null: Valid
+tests/why3/spec_memory.why Spec_memory INC_P: Valid
+tests/why3/spec_memory.why Spec_memory INC_A: Valid
+tests/why3/spec_memory.why Spec_memory INC_1: Valid
+tests/why3/spec_memory.why Spec_memory INC_2: Valid
+tests/why3/spec_memory.why Spec_memory INC_3: Valid
+tests/why3/spec_memory.why Spec_memory INC_4: Valid

src/plugins/wp/tests/why3/spec_memory.why

+module Spec_memory
+
+  use int.Int
+  use map.Map
+
+  use frama_c_wp.memory.Memory
+
+  type malloc = map int int
+
+  predicate spec_valid_rd (m: malloc) (p: addr) (n: int) =
+    if n <= 0 then true else
+    if p.base = 0 then false else
+    0 <= p.offset /\ p.offset + n <= m[p.base]
+
+  predicate spec_valid_rw (m: malloc) (p: addr) (n: int) =
+    if n <= 0 then true else
+    if p.base <= 0 then false else
+    0 <= p.offset /\ p.offset + n <= m[p.base]
+
+  predicate invalid_assigns (m: malloc) (p: addr) (n: int) =
+    forall k. 0 <= k < n -> not (valid_rd m (shift p k) 1)
+
+  goal check_valid_rd:
+    forall m p n. spec_valid_rd m p n <-> valid_rd m p n
+
+  goal check_valid:
+    forall m p n. spec_valid_rd m p n <-> valid_rd m p n
+
+  goal invalid_spec:
+    forall m p n.
+      invalid m p n -> invalid_assigns m p n
+
+  goal invalid_null_spec:
+    forall m n p.
+      p.base = 0 -> invalid m p n -> invalid_assigns m p n
+
+  goal invalid_null:
+    forall m n p.
+      p.base = 0 -> invalid m p n
+
+  goal invalid_empty:
+    forall m p n.
+       n <= 0 -> not (invalid m p n) -> invalid_assigns m p n
+
+  goal valid_rd_null:
+    forall m n p. p.base = 0 -> (n <= 0 <-> valid_rd m p n)
+
+  goal valid_rw_null:
+    forall m n p. p.base = 0 -> (n <= 0 <-> valid_rw m p n)
+
+  goal valid_obj_null:
+    forall m n. valid_obj m null n
+
+  (* included simplifier *)
+  goal INC_P:
+    forall p q a b.
+      p = q -> (included p a q b <-> ( 0 < a -> a <= b ))
+
+  goal INC_A:
+    forall p q a b.
+      a = b -> 0 < a ->
+        (included p a q b <->
+          (p.base = q.base /\ q.offset <= p.offset /\
+           p.offset + a <= q.offset + b))
+
+  goal INC_1:
+    forall p q a b.
+      a <= 0 -> (included p a q b <-> true)
+
+  goal INC_2:
+    forall p q a b.
+      b < 0 -> (included p a q b <-> a <= 0)
+
+  goal INC_3:
+    forall p q a b.
+      not
+        (p.base = q.base /\ q.offset <= p.offset /\
+         p.offset + a <= q.offset + b) ->
+        (included p a q b <-> a <= 0)
+
+  goal INC_4:
+    forall p q a b.
+      not a <= 0 -> not b < 0 ->
+        (included p a q b <->
+          (p.base = q.base /\ q.offset <= p.offset /\
+           p.offset + a <= q.offset + b))
+
+end

src/plugins/wp/tests/why3/test_config_qualif

+FILEREG: .*\.why
+CMD: why3 -L ./share/why3 prove -P alt-ergo
+OPT:
+FILTER: sed -e 's|\(.*\)\( (.*)\)|\1|'

src/plugins/wp/tests/wp_acsl/invalid_pointer.c

@@ -9,6 +9,8 @@ void memvar(void)
   //@check P2:  !\object_pointer(&x+2);
 }
 
+//@ logic char* GET = \null ;
+
 void pointer(void)
 {
   int x;
@@ -18,7 +20,8 @@ void pointer(void)
   //@check P0:   \object_pointer(p);
   //@check P1:   \object_pointer(p+1);
   //@check P2:  !\object_pointer(p+2);
-  //@check NULL: \object_pointer(\null);
+  //@check qed_NULL: \object_pointer(\null);
+  //@check prover_NULL: \object_pointer(GET);
 }
 
 void array(void)

src/plugins/wp/tests/wp_acsl/null.c

-
-#define NULL ((void*)0)
-
-//@ ensures \result == 0;
-int null_is_zero (void) {
-  void * p = NULL;
-  return (int) p;
-} 
-
-/*@ lemma valid_non_null:      !\valid     ((char *)\null); */
-/*@ lemma valid_read_non_null: !\valid_read((char *)\null); */
-
-

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

+
+//@ ensures \result == 0;
+int null_is_zero (void) {
+  void * p = (void*)0;
+  return (int) p;
+}
+
+/*@ lemma qed_not_valid_null:      !\valid     ((char *)\null); */
+/*@ lemma qed_not_valid_read_null: !\valid_read((char *)\null); */
+
+/*@ logic char* GET = \null ; */
+/*@ lemma prover_not_valid_null:      !\valid     ((char *)GET); */
+/*@ lemma prover_not_valid_read_null: !\valid_read((char *)GET); */
+
+
+// Prove null invalidity:
+
+//@ assigns *p;
+void qed_f(char *p);
+
+/*@ assigns \nothing; */
+void qed(){
+  qed_f(0);
+}
+
+//@ assigns *p;
+void prover_f(char *p);
+
+/*@ requires x == GET;
+    assigns \nothing; */
+void prover(char *x){
+  prover_f(x);
+}

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

@@ -2,68 +2,68 @@
 [kernel] Parsing tests/wp_acsl/invalid_pointer.c (with preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
-[wp] tests/wp_acsl/invalid_pointer.c:21: Warning: void object
+[wp] tests/wp_acsl/invalid_pointer.c:23: Warning: void object
 ------------------------------------------------------------
   Function array
 ------------------------------------------------------------
 
-Goal Check 'ARR' (file tests/wp_acsl/invalid_pointer.c, line 29):
+Goal Check 'ARR' (file tests/wp_acsl/invalid_pointer.c, line 32):
 Assume { Type: is_sint32(k). (* Heap *) Type: linked(Malloc_0). }
 Prove: ((0 <= k) /\ (k <= 25)) <->
-    valid_obj(Malloc_0[L_a_32 <- 25], shift_sint32(global(L_a_32), k), 1).
+    valid_obj(Malloc_0[L_a_33 <- 25], shift_sint32(global(L_a_33), k), 1).
 
 ------------------------------------------------------------
 ------------------------------------------------------------
   Function compound
 ------------------------------------------------------------
 
-Goal Check 'M1' (file tests/wp_acsl/invalid_pointer.c, line 44):
+Goal Check 'M1' (file tests/wp_acsl/invalid_pointer.c, line 47):
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Check 'P0' (file tests/wp_acsl/invalid_pointer.c, line 45):
+Goal Check 'P0' (file tests/wp_acsl/invalid_pointer.c, line 48):
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Check 'P1' (file tests/wp_acsl/invalid_pointer.c, line 46):
+Goal Check 'P1' (file tests/wp_acsl/invalid_pointer.c, line 49):
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Check 'P2' (file tests/wp_acsl/invalid_pointer.c, line 47):
+Goal Check 'P2' (file tests/wp_acsl/invalid_pointer.c, line 50):
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Check 'F' (file tests/wp_acsl/invalid_pointer.c, line 50):
+Goal Check 'F' (file tests/wp_acsl/invalid_pointer.c, line 53):
 Assume { (* Heap *) Type: linked(Malloc_0). }
-Prove: valid_obj(Malloc_0[L_s_37 <- 2], shiftfield_F1_S_f(global(L_s_37)), 1).
+Prove: valid_obj(Malloc_0[L_s_38 <- 2], shiftfield_F1_S_f(global(L_s_38)), 1).
 
 ------------------------------------------------------------
 
-Goal Check 'G' (file tests/wp_acsl/invalid_pointer.c, line 51):
+Goal Check 'G' (file tests/wp_acsl/invalid_pointer.c, line 54):
 Assume { (* Heap *) Type: linked(Malloc_0). }
-Prove: valid_obj(Malloc_0[L_s_37 <- 2], shiftfield_F1_S_g(global(L_s_37)), 1).
+Prove: valid_obj(Malloc_0[L_s_38 <- 2], shiftfield_F1_S_g(global(L_s_38)), 1).
 
 ------------------------------------------------------------
 
-Goal Check 'F2' (file tests/wp_acsl/invalid_pointer.c, line 52):
+Goal Check 'F2' (file tests/wp_acsl/invalid_pointer.c, line 55):
 Assume { (* Heap *) Type: linked(Malloc_0). }
-Prove: valid_obj(Malloc_0[L_s_37 <- 2],
-         shift_sint32(shiftfield_F1_S_f(global(L_s_37)), 2), 1).
+Prove: valid_obj(Malloc_0[L_s_38 <- 2],
+         shift_sint32(shiftfield_F1_S_f(global(L_s_38)), 2), 1).
 
 ------------------------------------------------------------
 
-Goal Check 'G2' (file tests/wp_acsl/invalid_pointer.c, line 53):
+Goal Check 'G2' (file tests/wp_acsl/invalid_pointer.c, line 56):
 Assume { (* Heap *) Type: linked(Malloc_0). }
-Prove: !valid_obj(Malloc_0[L_s_37 <- 2],
-          shift_sint32(shiftfield_F1_S_g(global(L_s_37)), 2), 1).
+Prove: !valid_obj(Malloc_0[L_s_38 <- 2],
+          shift_sint32(shiftfield_F1_S_g(global(L_s_38)), 2), 1).
 
 ------------------------------------------------------------
 
-Goal Check 'AM' (file tests/wp_acsl/invalid_pointer.c, line 56):
+Goal Check 'AM' (file tests/wp_acsl/invalid_pointer.c, line 59):
 Prove: true.
 
 ------------------------------------------------------------
@@ -94,32 +94,37 @@ Prove: true.
   Function pointer
 ------------------------------------------------------------
 
-Goal Check 'M1' (file tests/wp_acsl/invalid_pointer.c, line 17):
+Goal Check 'M1' (file tests/wp_acsl/invalid_pointer.c, line 19):
 Assume { (* Heap *) Type: linked(Malloc_0). }
-Prove: !valid_obj(Malloc_0[L_x_27 <- 1], shift_sint32(global(L_x_27), -1), 1).
+Prove: !valid_obj(Malloc_0[L_x_28 <- 1], shift_sint32(global(L_x_28), -1), 1).
 
 ------------------------------------------------------------
 
-Goal Check 'P0' (file tests/wp_acsl/invalid_pointer.c, line 18):
+Goal Check 'P0' (file tests/wp_acsl/invalid_pointer.c, line 20):
 Assume { (* Heap *) Type: linked(Malloc_0). }
-Prove: valid_obj(Malloc_0[L_x_27 <- 1], global(L_x_27), 1).
+Prove: valid_obj(Malloc_0[L_x_28 <- 1], global(L_x_28), 1).
 
 ------------------------------------------------------------
 
-Goal Check 'P1' (file tests/wp_acsl/invalid_pointer.c, line 19):
+Goal Check 'P1' (file tests/wp_acsl/invalid_pointer.c, line 21):
 Assume { (* Heap *) Type: linked(Malloc_0). }
-Prove: valid_obj(Malloc_0[L_x_27 <- 1], shift_sint32(global(L_x_27), 1), 1).
+Prove: valid_obj(Malloc_0[L_x_28 <- 1], shift_sint32(global(L_x_28), 1), 1).
 
 ------------------------------------------------------------
 
-Goal Check 'P2' (file tests/wp_acsl/invalid_pointer.c, line 20):
+Goal Check 'P2' (file tests/wp_acsl/invalid_pointer.c, line 22):
 Assume { (* Heap *) Type: linked(Malloc_0). }
-Prove: !valid_obj(Malloc_0[L_x_27 <- 1], shift_sint32(global(L_x_27), 2), 1).
+Prove: !valid_obj(Malloc_0[L_x_28 <- 1], shift_sint32(global(L_x_28), 2), 1).
 
 ------------------------------------------------------------
 
-Goal Check 'NULL' (file tests/wp_acsl/invalid_pointer.c, line 21):
+Goal Check 'qed_NULL' (file tests/wp_acsl/invalid_pointer.c, line 23):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'prover_NULL' (file tests/wp_acsl/invalid_pointer.c, line 24):
 Assume { (* Heap *) Type: linked(Malloc_0). }
-Prove: valid_obj(Malloc_0[L_x_27 <- 1], null, 1).
+Prove: valid_obj(Malloc_0[L_x_28 <- 1], L_GET, 1).
 
 ------------------------------------------------------------

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

 # frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/null.c (with preprocessing)
+[kernel] Parsing tests/wp_acsl/null.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
 ------------------------------------------------------------
   Global
 ------------------------------------------------------------
 
-Lemma valid_non_null:
-Prove: not (valid_rw Malloc_0 null 1)
+Lemma prover_not_valid_null:
+Assume: 'qed_not_valid_read_null' 'qed_not_valid_null'
+Prove: not (valid_rw Malloc_0 L_GET 1)
 
 ------------------------------------------------------------
 
-Lemma valid_read_non_null:
-Assume: 'valid_non_null'
-Prove: not (valid_rd Malloc_0 null 1)
+Lemma prover_not_valid_read_null:
+Assume: 'prover_not_valid_null' 'qed_not_valid_read_null'
+  'qed_not_valid_null'
+Prove: not (valid_rd Malloc_0 L_GET 1)
+
+------------------------------------------------------------
+
+Lemma qed_not_valid_null:
+Prove: true
+
+------------------------------------------------------------
+
+Lemma qed_not_valid_read_null:
+Assume: 'qed_not_valid_null'
+Prove: true
 
 ------------------------------------------------------------
 ------------------------------------------------------------
   Function null_is_zero
 ------------------------------------------------------------
 
-Goal Post-condition (file tests/wp_acsl/null.c, line 4) in 'null_is_zero':
+Goal Post-condition (file tests/wp_acsl/null.i, line 2) in 'null_is_zero':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function prover
+------------------------------------------------------------
+
+Goal Assigns nothing in 'prover':
+Call Effect at line 32
+Assume { (* Heap *) Type: linked(Malloc_0). }
+Prove: invalid(Malloc_0, L_GET, 1).
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'prover':
+Call Effect at line 32
+Assume { (* Heap *) Type: linked(Malloc_0). }
+Prove: invalid(Malloc_0, L_GET, 1).
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function qed
+------------------------------------------------------------
+
+Goal Assigns nothing in 'qed':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'qed':
 Prove: true.
 
 ------------------------------------------------------------

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

@@ -2,8 +2,8 @@
 [kernel] Parsing tests/wp_acsl/invalid_pointer.c (with preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
-[wp] tests/wp_acsl/invalid_pointer.c:21: Warning: void object
-[wp] 19 goals scheduled
+[wp] tests/wp_acsl/invalid_pointer.c:23: Warning: void object
+[wp] 20 goals scheduled
 [wp] [Qed] Goal typed_memvar_check_M1 : Valid
 [wp] [Qed] Goal typed_memvar_check_P0 : Valid
 [wp] [Qed] Goal typed_memvar_check_P1 : Valid
@@ -12,7 +12,8 @@
 [wp] [Alt-Ergo] Goal typed_pointer_check_P0 : Valid
 [wp] [Alt-Ergo] Goal typed_pointer_check_P1 : Valid
 [wp] [Alt-Ergo] Goal typed_pointer_check_P2 : Valid
-[wp] [Alt-Ergo] Goal typed_pointer_check_NULL : Valid
+[wp] [Qed] Goal typed_pointer_check_qed_NULL : Valid
+[wp] [Alt-Ergo] Goal typed_pointer_check_prover_NULL : Valid
 [wp] [Alt-Ergo] Goal typed_array_check_ARR : Valid
 [wp] [Qed] Goal typed_compound_check_M1 : Valid
 [wp] [Qed] Goal typed_compound_check_P0 : Valid
@@ -23,13 +24,13 @@
 [wp] [Alt-Ergo] Goal typed_compound_check_F2 : Valid
 [wp] [Alt-Ergo] Goal typed_compound_check_G2 : Valid
 [wp] [Qed] Goal typed_compound_check_AM : Valid
-[wp] Proved goals:   19 / 19
-  Qed:             9 
+[wp] Proved goals:   20 / 20
+  Qed:            10 
   Alt-Ergo:       10
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
   memvar                    4        -        4       100%
-  pointer                   -        5        5       100%
+  pointer                   1        5        6       100%
   array                     -        1        1       100%
   compound                  5        4        9       100%
 ------------------------------------------------------------

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

 # frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/null.c (with preprocessing)
+[kernel] Parsing tests/wp_acsl/null.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
-[wp] 3 goals scheduled
-[wp] [Alt-Ergo] Goal typed_lemma_valid_non_null : Valid
-[wp] [Alt-Ergo] Goal typed_lemma_valid_read_non_null : Valid
+[wp] 9 goals scheduled
+[wp] [Alt-Ergo] Goal typed_lemma_prover_not_valid_null : Valid
+[wp] [Alt-Ergo] Goal typed_lemma_prover_not_valid_read_null : Valid
+[wp] [Qed] Goal typed_lemma_qed_not_valid_null : Valid
+[wp] [Qed] Goal typed_lemma_qed_not_valid_read_null : Valid
 [wp] [Qed] Goal typed_null_is_zero_ensures : Valid
-[wp] Proved goals:    3 / 3
-  Qed:             1 
-  Alt-Ergo:        2
+[wp] [Qed] Goal typed_qed_assigns_exit : Valid
+[wp] [Qed] Goal typed_qed_assigns_normal : Valid
+[wp] [Alt-Ergo] Goal typed_prover_assigns_exit : Valid
+[wp] [Alt-Ergo] Goal typed_prover_assigns_normal : Valid
+[wp] Proved goals:    9 / 9
+  Qed:             5 
+  Alt-Ergo:        4
 ------------------------------------------------------------
  Axiomatics                WP     Alt-Ergo  Total   Success
-  Lemma                     -        2        2       100%
+  Lemma                     2        2        4       100%
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
   null_is_zero              1        -        1       100%
+  qed                       2        -        2       100%
+  prover                    -        2        2       100%
 ------------------------------------------------------------