[wp] Fix frame condition

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

@@ -111,7 +111,7 @@ theory Memory
   predicate linked (map int int)
   predicate sconst (map addr int)
   predicate framed (m : map addr addr) =
-    forall p:addr [m[p]]. region(m[p].base) <= 0
+    forall p:addr [m[p]]. region(p.base) <= 0 -> region(m[p].base) <= 0
 
   (* Properties *)
 

src/plugins/wp/tests/wp_typed/frame.i

@@ -14,3 +14,23 @@ void compound(int k) {
 // NOTE:
 // if we require \valid(comp[k].ptr) the goal is provable without frame conditions
 // since it can not be aliased with 'm' at PRE, which is not (yet) valid.
+
+// For those two examples, we want the assert false to fail:
+//  -> the frame condition must *not* introduce incoherence on initialization
+
+void local_region(void) {
+  char b[4] = {0};
+  char *x = b ;
+  char **in_memtyped = &x ; // be sure to put x in MemTyped
+  //@ assert A:X: \valid_read(x + (0..3));
+  //@ assert A:Y: \false ;
+}
+
+struct S { char b ; };
+
+void formal_region(struct S s) {
+  char *x = &s.b ;
+  char **in_memtyped = &x ; // be sure to put x in MemTyped
+  //@ assert A:X: \valid_read(x);
+  //@ assert A:Y: \false ;
+}

src/plugins/wp/tests/wp_typed/oracle/frame.0.res.oracle

@@ -38,3 +38,61 @@ Assume {
 Prove: x = 1.
 
 ------------------------------------------------------------
+------------------------------------------------------------
+  Function formal_region
+------------------------------------------------------------
+
+Goal Assertion 'A,X' (file tests/wp_typed/frame.i, line 34):
+Let a = Mptr_0[global(L_x_37)].
+Assume {
+  (* Heap *)
+  Type: framed(Mptr_0) /\ linked(Malloc_0).
+  (* Initializer *)
+  Init: a = shiftfield_F2_S_b(global(P_s_36)).
+}
+Prove: valid_rd(Malloc_0[P_s_36 <- 1][L_x_37 <- 1], a, 1).
+
+------------------------------------------------------------
+
+Goal Assertion 'A,Y' (file tests/wp_typed/frame.i, line 35):
+Let a = Mptr_0[global(L_x_37)].
+Assume {
+  (* Heap *)
+  Type: framed(Mptr_0) /\ linked(Malloc_0).
+  (* Initializer *)
+  Init: a = shiftfield_F2_S_b(global(P_s_36)).
+  (* Assertion 'A,X' *)
+  Have: valid_rd(Malloc_0[P_s_36 <- 1][L_x_37 <- 1], a, 1).
+}
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function local_region
+------------------------------------------------------------
+
+Goal Assertion 'A,X' (file tests/wp_typed/frame.i, line 25):
+Let a = Mptr_0[global(L_x_32)].
+Assume {
+  (* Heap *)
+  Type: framed(Mptr_0) /\ linked(Malloc_0).
+  (* Initializer *)
+  Init: a = shift_sint8(global(L_b_31), 0).
+}
+Prove: valid_rd(Malloc_0[L_b_31 <- 4][L_x_32 <- 1], a, 4).
+
+------------------------------------------------------------
+
+Goal Assertion 'A,Y' (file tests/wp_typed/frame.i, line 26):
+Let a = Mptr_0[global(L_x_32)].
+Assume {
+  (* Heap *)
+  Type: framed(Mptr_0) /\ linked(Malloc_0).
+  (* Initializer *)
+  Init: a = shift_sint8(global(L_b_31), 0).
+  (* Assertion 'A,X' *)
+  Have: valid_rd(Malloc_0[L_b_31 <- 4][L_x_32 <- 1], a, 4).
+}
+Prove: false.
+
+------------------------------------------------------------

src/plugins/wp/tests/wp_typed/oracle/frame.1.res.oracle

@@ -38,3 +38,61 @@ Assume {
 Prove: x = 1.
 
 ------------------------------------------------------------
+------------------------------------------------------------
+  Function formal_region
+------------------------------------------------------------
+
+Goal Assertion 'A,X' (file tests/wp_typed/frame.i, line 34):
+Let a = Mptr_0[global(L_x_37)].
+Assume {
+  (* Heap *)
+  Type: framed(Mptr_0) /\ linked(Malloc_0).
+  (* Initializer *)
+  Init: a = shiftfield_F2_S_b(global(P_s_36)).
+}
+Prove: valid_rd(Malloc_0[P_s_36 <- 1][L_x_37 <- 1], a, 1).
+
+------------------------------------------------------------
+
+Goal Assertion 'A,Y' (file tests/wp_typed/frame.i, line 35):
+Let a = Mptr_0[global(L_x_37)].
+Assume {
+  (* Heap *)
+  Type: framed(Mptr_0) /\ linked(Malloc_0).
+  (* Initializer *)
+  Init: a = shiftfield_F2_S_b(global(P_s_36)).
+  (* Assertion 'A,X' *)
+  Have: valid_rd(Malloc_0[P_s_36 <- 1][L_x_37 <- 1], a, 1).
+}
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function local_region
+------------------------------------------------------------
+
+Goal Assertion 'A,X' (file tests/wp_typed/frame.i, line 25):
+Let a = Mptr_0[global(L_x_32)].
+Assume {
+  (* Heap *)
+  Type: framed(Mptr_0) /\ linked(Malloc_0).
+  (* Initializer *)
+  Init: a = shift_sint8(global(L_b_31), 0).
+}
+Prove: valid_rd(Malloc_0[L_b_31 <- 4][L_x_32 <- 1], a, 4).
+
+------------------------------------------------------------
+
+Goal Assertion 'A,Y' (file tests/wp_typed/frame.i, line 26):
+Let a = Mptr_0[global(L_x_32)].
+Assume {
+  (* Heap *)
+  Type: framed(Mptr_0) /\ linked(Malloc_0).
+  (* Initializer *)
+  Init: a = shift_sint8(global(L_b_31), 0).
+  (* Assertion 'A,X' *)
+  Have: valid_rd(Malloc_0[L_b_31 <- 4][L_x_32 <- 1], a, 4).
+}
+Prove: false.
+
+------------------------------------------------------------

src/plugins/wp/tests/wp_typed/oracle_qualif/frame.res.oracle

@@ -2,13 +2,19 @@
 [kernel] Parsing tests/wp_typed/frame.i (no preprocessing)
 [wp] Running WP plugin...
 [wp] Warning: Missing RTE guards
-[wp] 2 goals scheduled
+[wp] 6 goals scheduled
 [wp] [Alt-Ergo] Goal typed_compound_assert_SEP : Unsuccess
 [wp] [Alt-Ergo] Goal typed_compound_assert_RES : Valid
-[wp] Proved goals:    1 / 2
+[wp] [Alt-Ergo] Goal typed_local_region_assert_A_X : Valid
+[wp] [Alt-Ergo] Goal typed_local_region_assert_A_Y : Unsuccess
+[wp] [Alt-Ergo] Goal typed_formal_region_assert_A_X : Valid
+[wp] [Alt-Ergo] Goal typed_formal_region_assert_A_Y : Unsuccess
+[wp] Proved goals:    3 / 6
   Qed:             0 
-  Alt-Ergo:        1  (unsuccess: 1)
+  Alt-Ergo:        3  (unsuccess: 3)
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
   compound                  -        1        2      50.0%
+  local_region              -        1        2      50.0%
+  formal_region             -        1        2      50.0%
 ------------------------------------------------------------

src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json

@@ -3,8 +3,8 @@
                 "target": "exists i_0,i_1:int.\n(i_0<=i_136) /\\ (i_1<=i_137) /\\ (0<=i_0) /\\ (i_136<=i_0) /\\ (i_137<=i_1)\n/\\ (i_0<=9)",
                 "pattern": "\\E$i$i0$i$i9" },
     "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
-                                  "verdict": "valid", "time": 0.0109,
+                                  "verdict": "valid", "time": 0.0088,
                                   "steps": 24 } ],
                   "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
-                                  "verdict": "valid", "time": 0.0114,
+                                  "verdict": "valid", "time": 0.0116,
                                   "steps": 24 } ] } } ]

src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json

@@ -3,8 +3,8 @@
                 "target": "exists i_0,i_1:int.\n(i_0<=i_136) /\\ (i_1<=i_137) /\\ (0<=i_0) /\\ (i_136<=i_0) /\\ (i_137<=i_1)\n/\\ (i_0<=9)",
                 "pattern": "\\E$i$i0$i$i9" },
     "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
-                                  "verdict": "valid", "time": 0.0109,
+                                  "verdict": "valid", "time": 0.0088,
                                   "steps": 24 } ],
                   "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
-                                  "verdict": "valid", "time": 0.0114,
+                                  "verdict": "valid", "time": 0.0116,
                                   "steps": 24 } ] } } ]

src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json

@@ -3,8 +3,8 @@
                 "target": "exists i_0,i_1:int.\n(i_0<=i_9) /\\ (i_1<=i_10) /\\ (0<=i_0) /\\ (i_9<=i_0) /\\ (i_10<=i_1)\n/\\ (i_0<=9)",
                 "pattern": "\\E$i$i0$i$i9" },
     "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
-                                  "verdict": "valid", "time": 0.0151,
+                                  "verdict": "valid", "time": 0.0279,
                                   "steps": 41 } ],
                   "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
-                                  "verdict": "valid", "time": 0.0147,
+                                  "verdict": "valid", "time": 0.021,
                                   "steps": 41 } ] } } ]

src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json

@@ -3,8 +3,8 @@
                 "target": "exists i_1,i_2:int.\n(i_1<=i_0) /\\ (i_2<=i_3) /\\ (0<=i_1) /\\ (i_0<=i_1) /\\ (i_3<=i_2) /\\ (i_1<=9)",
                 "pattern": "\\E$i$i0$i$i9" },
     "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.2.0",
-                                  "verdict": "valid", "time": 0.0115,
+                                  "verdict": "valid", "time": 0.009,
                                   "steps": 29 } ],
                   "Goal 2/2": [ { "prover": "Alt-Ergo:2.2.0",
-                                  "verdict": "valid", "time": 0.0117,
+                                  "verdict": "valid", "time": 0.0131,
                                   "steps": 29 } ] } } ]