diff --git a/src/plugins/wp/MemMemory.ml b/src/plugins/wp/MemMemory.ml
index c0f4455e346f80cef268f23714e327dd9427e8d3..bab9e05ecf91a2b75e6a4f466a574eb987007bf0 100644
--- a/src/plugins/wp/MemMemory.ml
+++ b/src/plugins/wp/MemMemory.ml
@@ -341,6 +341,28 @@ let phi_addr_of_int p =
| L.Fun(f,[a]) when f == f_int_of_addr -> a
| _ -> raise Not_found
+(* -------------------------------------------------------------------------- *)
+(* --- Simplifier for (in)validity --- *)
+(* -------------------------------------------------------------------------- *)
+
+(* Lemmas proved with Memory definition:
+ - lemma valid_rd_null: forall m n. n <= 0 -> valid_rd m null n
+ - lemma valid_rw_null: forall m n. n <= 0 -> valid_rw m null n *)
+let r_valid_unref = function
+ | [_; p; n] when p == a_null -> e_leq n e_zero
+ | _ -> raise Not_found
+
+(* Lemmas proved with Memory definition:
+ - lemma valid_obj_null: forall m n. valid_obj m null n *)
+let r_valid_obj = function
+ | [_; p; _] when p == a_null -> e_true
+ | _ -> raise Not_found
+
+(* Condition: by definition of 'invalid_null' *)
+let r_invalid = function
+ | [_; p; n] when p == a_null -> e_neq e_zero n
+ | _ -> raise Not_found
+
(* -------------------------------------------------------------------------- *)
(* --- Simplifiers Registration --- *)
(* -------------------------------------------------------------------------- *)
@@ -358,6 +380,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
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/share/why3/frama_c_wp/memory.mlw b/src/plugins/wp/share/why3/frama_c_wp/memory.mlw
index c2f0cc8634b86158a92d04f49095291a20c0e8b9..b0cee81bfe10164fe4d253639781d2afa2aaa475 100644
--- a/src/plugins/wp/share/why3/frama_c_wp/memory.mlw
+++ b/src/plugins/wp/share/why3/frama_c_wp/memory.mlw
@@ -95,6 +95,9 @@ theory Memory
0 <= p.offset < m[p.base] ->
(valid_rd m p 1 /\ not (valid_rw m p 1))
+ lemma invalid_null :
+ forall m : map int int, n: int. n <> 0 -> invalid m null n
+
lemma separated_1 : forall p q : addr. forall a b i j : int
[ separated p a q b , { base = p.base ; offset = i } ,
{ base = q.base ; offset = j } ].
diff --git a/src/plugins/wp/tests/wp_acsl/invalid_pointer.c b/src/plugins/wp/tests/wp_acsl/invalid_pointer.c
index 14e08fdd4b9061d204f19f7699b5b58dea6492e8..b1e5a2f0f9ad8cd393ff689c00afb36926be0c0b 100644
--- a/src/plugins/wp/tests/wp_acsl/invalid_pointer.c
+++ b/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)
diff --git a/src/plugins/wp/tests/wp_acsl/null.c b/src/plugins/wp/tests/wp_acsl/null.c
deleted file mode 100644
index 62bcf566c7cf2af918325763e88facb763e04bef..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_acsl/null.c
+++ /dev/null
@@ -1,13 +0,0 @@
-
-#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); */
-
-
diff --git a/src/plugins/wp/tests/wp_acsl/null.i b/src/plugins/wp/tests/wp_acsl/null.i
new file mode 100644
index 0000000000000000000000000000000000000000..7f84ed13cc1de68b2dffe4647e1ce27150adf6c7
--- /dev/null
+++ b/src/plugins/wp/tests/wp_acsl/null.i
@@ -0,0 +1,33 @@
+
+//@ 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);
+}
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/invalid_pointer.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/invalid_pointer.res.oracle
index a9d75cace6c480bb82fe3bd6f959244041928bb4..cff34f592b2de8157a1e9ea9411d3ed97bfd6d49 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/invalid_pointer.res.oracle
+++ b/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).
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/null.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/null.res.oracle
index 16ac874aa695270bd9cf2784c559eb4e32c7fa23..00b77b3dcea936a0e7cf583c9c108f1a593d0cdc 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/null.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/null.res.oracle
@@ -1,26 +1,69 @@
# 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.
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.res.oracle
index 089501d0a3a6713dce8e372db5c147a9a61e7bbb..11bf83472b124a30221db889001dc6dfa817ab1c 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.res.oracle
+++ b/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%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/null.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/null.res.oracle
index 1f8e9e4734906168f09d6bb3896f221f95211933..f6bf4365dd2b449a6176341fb32ff4cfe95c3700 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/null.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/null.res.oracle
@@ -1,18 +1,26 @@
# 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%
------------------------------------------------------------