[wp] test for invalid pointers

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

@@ -76,7 +76,8 @@ theory Memory
     n > 0 -> ( 0 <> p.base /\ 0 <= p.offset /\ p.offset + n <= m[p.base] )
 
   predicate valid_obj (m : map int int) (p:addr) (n:int) =
-    n > 0 -> ( 0 <> p.base /\ 0 <= p.offset /\ p.offset + n <= 1 + m[p.base] )
+    n > 0 -> ( p = null \/
+             ( 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 )

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

+/* Tests for \object_pointer() */
+
+void memvar(void)
+{
+  int x;
+  //@check M1:  !\object_pointer(&x-1);
+  //@check P0:   \object_pointer(&x);
+  //@check P1:   \object_pointer(&x+1);
+  //@check P2:  !\object_pointer(&x+2);
+}
+
+void pointer(void)
+{
+  int x;
+  int *p = &x ;
+  *p = 1 ;
+  //@check M1:  !\object_pointer(p-1);
+  //@check P0:   \object_pointer(p);
+  //@check P1:   \object_pointer(p+1);
+  //@check P2:  !\object_pointer(p+2);
+  //@check NULL: \object_pointer(\null);
+}
+
+void array(void)
+{
+  int k;
+  int a[25];
+  int *q = &a[k];
+  //@check ARR: (0 <= k <= 25) <==> \object_pointer(q);
+}
+
+struct S {
+  int f ;
+  int g ;
+};
+
+struct A {
+  int m[10];
+};
+
+void compound(void)
+{
+  struct S u ;
+  //@check M1: !\object_pointer(&u-1);
+  //@check P0:  \object_pointer(&u);
+  //@check P1:  \object_pointer(&u+1);
+  //@check P2: !\object_pointer(&u+2);
+  struct S s ;
+  struct S *p = &s ;
+  //@check F:   \object_pointer(&(p->f));
+  //@check G:   \object_pointer(&(p->g));
+  //@check F2:  \object_pointer(&(p->f)+2);
+  //@check G2: !\object_pointer(&(p->g)+2);
+  int k ;
+  struct A a ;
+  //@check AM: (0 <= k <= 10) <==> \object_pointer(&a.m[k]);
+}

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

+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/invalid_pointer.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] tests/wp_acsl/invalid_pointer.c:21: Warning: void object
+------------------------------------------------------------
+  Function array
+------------------------------------------------------------
+
+Goal Check 'ARR' (file tests/wp_acsl/invalid_pointer.c, line 29):
+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).
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function compound
+------------------------------------------------------------
+
+Goal Check 'M1' (file tests/wp_acsl/invalid_pointer.c, line 44):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'P0' (file tests/wp_acsl/invalid_pointer.c, line 45):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'P1' (file tests/wp_acsl/invalid_pointer.c, line 46):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'P2' (file tests/wp_acsl/invalid_pointer.c, line 47):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'F' (file tests/wp_acsl/invalid_pointer.c, line 50):
+Assume { (* Heap *) Type: linked(Malloc_0). }
+Prove: valid_obj(Malloc_0[L_s_37 <- 2], shiftfield_F1_S_f(global(L_s_37)), 1).
+
+------------------------------------------------------------
+
+Goal Check 'G' (file tests/wp_acsl/invalid_pointer.c, line 51):
+Assume { (* Heap *) Type: linked(Malloc_0). }
+Prove: valid_obj(Malloc_0[L_s_37 <- 2], shiftfield_F1_S_g(global(L_s_37)), 1).
+
+------------------------------------------------------------
+
+Goal Check 'F2' (file tests/wp_acsl/invalid_pointer.c, line 52):
+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).
+
+------------------------------------------------------------
+
+Goal Check 'G2' (file tests/wp_acsl/invalid_pointer.c, line 53):
+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).
+
+------------------------------------------------------------
+
+Goal Check 'AM' (file tests/wp_acsl/invalid_pointer.c, line 56):
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function memvar
+------------------------------------------------------------
+
+Goal Check 'M1' (file tests/wp_acsl/invalid_pointer.c, line 6):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'P0' (file tests/wp_acsl/invalid_pointer.c, line 7):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'P1' (file tests/wp_acsl/invalid_pointer.c, line 8):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Check 'P2' (file tests/wp_acsl/invalid_pointer.c, line 9):
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function pointer
+------------------------------------------------------------
+
+Goal Check 'M1' (file tests/wp_acsl/invalid_pointer.c, line 17):
+Assume { (* Heap *) Type: linked(Malloc_0). }
+Prove: !valid_obj(Malloc_0[L_x_27 <- 1], shift_sint32(global(L_x_27), -1), 1).
+
+------------------------------------------------------------
+
+Goal Check 'P0' (file tests/wp_acsl/invalid_pointer.c, line 18):
+Assume { (* Heap *) Type: linked(Malloc_0). }
+Prove: valid_obj(Malloc_0[L_x_27 <- 1], global(L_x_27), 1).
+
+------------------------------------------------------------
+
+Goal Check 'P1' (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).
+
+------------------------------------------------------------
+
+Goal Check 'P2' (file tests/wp_acsl/invalid_pointer.c, line 20):
+Assume { (* Heap *) Type: linked(Malloc_0). }
+Prove: !valid_obj(Malloc_0[L_x_27 <- 1], shift_sint32(global(L_x_27), 2), 1).
+
+------------------------------------------------------------
+
+Goal Check 'NULL' (file tests/wp_acsl/invalid_pointer.c, line 21):
+Assume { (* Heap *) Type: linked(Malloc_0). }
+Prove: valid_obj(Malloc_0[L_x_27 <- 1], null, 1).
+
+------------------------------------------------------------

src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.0.session/cache/546d68cf73aa7d1be7397f0dba7ab57b.json

+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0104,
+  "steps": 15 }

src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.0.session/cache/6135a695451f38570cc5e98d983b3fc5.json

+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0128,
+  "steps": 10 }

src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.0.session/cache/82fda005a00dfb2bafda2e7a61e31a0e.json

+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0105,
+  "steps": 15 }

src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.0.session/cache/a09f29e9995f66e54188484d0f6a022c.json

+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.01, "steps": 14 }

src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.0.session/cache/a1789ac93bbdd1b61d2668d397e828b5.json

+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0087,
+  "steps": 8 }

src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.0.session/cache/a66c1f9591316a451c831ed9aa33375a.json

+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0099,
+  "steps": 10 }

src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.0.session/cache/bff665fbed54b18d00114b87eaddf2d7.json

+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0149,
+  "steps": 22 }

src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.0.session/cache/e73bf6bee511f053358c2e0d3561a7e1.json

+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0116,
+  "steps": 15 }

src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.0.session/cache/edc73eb8a8cf742d31cbce5dfed79215.json

+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.0106,
+  "steps": 16 }

src/plugins/wp/tests/wp_acsl/oracle_qualif/invalid_pointer.0.session/cache/f957b00472bc5ec2c8193749f227c435.json

+{ "prover": "Alt-Ergo:2.0.0", "verdict": "valid", "time": 0.01, "steps": 11 }

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

+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/invalid_pointer.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] tests/wp_acsl/invalid_pointer.c:21: Warning: void object
+[wp] 19 goals scheduled
+[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
+[wp] [Qed] Goal typed_compound_check_P1 : Valid
+[wp] [Qed] Goal typed_compound_check_P2 : Valid
+[wp] [Alt-Ergo] Goal typed_compound_check_F : Valid
+[wp] [Alt-Ergo] Goal typed_compound_check_G : Valid
+[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] [Qed] Goal typed_memvar_check_M1 : Valid
+[wp] [Qed] Goal typed_memvar_check_P0 : Valid
+[wp] [Qed] Goal typed_memvar_check_P1 : Valid
+[wp] [Qed] Goal typed_memvar_check_P2 : Valid
+[wp] [Alt-Ergo] Goal typed_pointer_check_M1 : Valid
+[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] Proved goals:   19 / 19
+  Qed:             9 
+  Alt-Ergo:       10
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  memvar                    4        -        4       100%
+  pointer                   -        5        5       100%
+  array                     -        1        1       100%
+  compound                  5        4        9       100%
+------------------------------------------------------------