[wp] MemVar: normalize offset on initialized array

src/plugins/wp/MemVar.ml

@@ -1103,6 +1103,13 @@ struct
                   let l = mloc_of_loc l in
                   M.initialized sigma.mem (Rrange(l,elt,Some a, Some b))
                 else
+                  let rec normalize obj = function
+                    | [] -> [], Extlib.id
+                    | [Shift(elt, i)] when Ctypes.equal obj elt -> [], F.e_add i
+                    | f :: ofs -> let l, fn = normalize obj ofs in f :: l, fn
+                  in
+                  let p, shift = normalize elt p in
+                  let a = shift a and b = shift b in
                   let in_array = valid_range RW (vobject m x) p (elt, a, b) in
                   let initialized =
                     if x.vformal || x.vglob then p_true

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

+/*@
+  requires \initialized(buf + (0 .. count - 1));
+*/
+int test(char *buf, int count);
+
+// Success:
+
+void succ_full_first_cell(void){
+  char buf[3] = {0};
+  test(buf    , 1);
+}
+void succ_full_full(void){
+  char buf[3] = {0};
+	test(&buf[0], 3);
+}
+void succ_full_from_1(void){
+  char buf[3] = {0};
+	test(buf+1  , 2);
+}
+void succ_from_1_from_1(void){
+  char buf[3];
+	buf[1] = buf[2] = 1 ;
+	test(buf+1  , 2);
+}
+void succ_full_from_2(void){
+  char buf[3] = {0};
+	test(&buf[2], 1);
+}
+
+// Failure:
+
+void fail_cell_before(void){
+  char buf[3] = {0};
+	test(buf-1  , 1);
+}
+void fail_too_long(void){
+  char buf[3] = {0};
+	test(buf    , 4);
+}
+void fail_too_long_from_1(void){
+  char buf[3] = {0};
+	test(&buf[1], 3);
+}
+void fail_too_long_from_2(void){
+  char buf[3] = {0};
+  test(buf+2  , 2);
+}
+void fail_cell_after_end(void){
+  char buf[3] = {0};
+	test(buf+3  , 1);
+}
+void fail_partial_not_full(void){
+  char buf[3];
+	buf[0] = buf[1] = 0;
+	test(&buf[0], 3);
+}

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

+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/initialized_shift_array.i (no preprocessing)
+[wp] Running WP plugin...
+[kernel] tests/wp_acsl/initialized_shift_array.i:52: Warning: 
+  No code nor implicit assigns clause for function test, generating default assigns from the prototype
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function fail_cell_after_end
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_acsl/initialized_shift_array.i, line 2) in 'test'' in 'fail_cell_after_end' at call 'test' (file tests/wp_acsl/initialized_shift_array.i, line 50)
+:
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function fail_cell_before
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_acsl/initialized_shift_array.i, line 2) in 'test'' in 'fail_cell_before' at call 'test' (file tests/wp_acsl/initialized_shift_array.i, line 34)
+:
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function fail_partial_not_full
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_acsl/initialized_shift_array.i, line 2) in 'test'' in 'fail_partial_not_full' at call 'test' (file tests/wp_acsl/initialized_shift_array.i, line 55)
+:
+Assume { (* Goal *) When: (0 <= i) /\ (i <= 2). }
+Prove: (([false..])[1 <- true][0 <- true][i]=true).
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function fail_too_long
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_acsl/initialized_shift_array.i, line 2) in 'test'' in 'fail_too_long' at call 'test' (file tests/wp_acsl/initialized_shift_array.i, line 38)
+:
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function fail_too_long_from_1
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_acsl/initialized_shift_array.i, line 2) in 'test'' in 'fail_too_long_from_1' at call 'test' (file tests/wp_acsl/initialized_shift_array.i, line 42)
+:
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function fail_too_long_from_2
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_acsl/initialized_shift_array.i, line 2) in 'test'' in 'fail_too_long_from_2' at call 'test' (file tests/wp_acsl/initialized_shift_array.i, line 46)
+:
+Prove: false.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function succ_from_1_from_1
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_acsl/initialized_shift_array.i, line 2) in 'test'' in 'succ_from_1_from_1' at call 'test' (file tests/wp_acsl/initialized_shift_array.i, line 23)
+:
+Assume { (* Goal *) When: (0 < i) /\ (i <= 2). }
+Prove: (([false..])[2 <- true][1 <- true][i]=true).
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function succ_full_first_cell
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_acsl/initialized_shift_array.i, line 2) in 'test'' in 'succ_full_first_cell' at call 'test' (file tests/wp_acsl/initialized_shift_array.i, line 10)
+:
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function succ_full_from_1
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_acsl/initialized_shift_array.i, line 2) in 'test'' in 'succ_full_from_1' at call 'test' (file tests/wp_acsl/initialized_shift_array.i, line 18)
+:
+Assume {
+  (* Goal *)
+  When: (0 < i) /\ (i <= 2).
+  (* Initializer *)
+  Init: (Init_buf_0[0]=true).
+  (* Initializer *)
+  Init: forall i_1 : Z. ((0 < i_1) -> ((i_1 <= 2) ->
+      (Init_buf_0[i_1]=true))).
+}
+Prove: (Init_buf_0[i]=true).
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function succ_full_from_2
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_acsl/initialized_shift_array.i, line 2) in 'test'' in 'succ_full_from_2' at call 'test' (file tests/wp_acsl/initialized_shift_array.i, line 27)
+:
+Assume {
+  (* Goal *)
+  When: (2 <= i) /\ (i <= 2).
+  (* Initializer *)
+  Init: (Init_buf_0[0]=true).
+  (* Initializer *)
+  Init: forall i_1 : Z. ((0 < i_1) -> ((i_1 <= 2) ->
+      (Init_buf_0[i_1]=true))).
+}
+Prove: (Init_buf_0[2]=true).
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function succ_full_full
+------------------------------------------------------------
+
+Goal Instance of 'Pre-condition (file tests/wp_acsl/initialized_shift_array.i, line 2) in 'test'' in 'succ_full_full' at call 'test' (file tests/wp_acsl/initialized_shift_array.i, line 14)
+:
+Assume {
+  (* Goal *)
+  When: (0 <= i) /\ (i <= 2).
+  (* Initializer *)
+  Init: (Init_buf_0[0]=true).
+  (* Initializer *)
+  Init: forall i_1 : Z. ((0 < i_1) -> ((i_1 <= 2) ->
+      (Init_buf_0[i_1]=true))).
+}
+Prove: (Init_buf_0[i]=true).
+
+------------------------------------------------------------

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

+# frama-c -wp [...]
+[kernel] Parsing tests/wp_acsl/initialized_shift_array.i (no preprocessing)
+[wp] Running WP plugin...
+[kernel] tests/wp_acsl/initialized_shift_array.i:52: Warning: 
+  No code nor implicit assigns clause for function test, generating default assigns from the prototype
+[wp] Warning: Missing RTE guards
+[wp] 11 goals scheduled
+[wp] [Qed] Goal typed_succ_full_first_cell_call_test_requires : Valid
+[wp] [Alt-Ergo] Goal typed_succ_full_full_call_test_requires : Valid
+[wp] [Alt-Ergo] Goal typed_succ_full_from_1_call_test_requires : Valid
+[wp] [Alt-Ergo] Goal typed_succ_from_1_from_1_call_test_requires : Valid
+[wp] [Alt-Ergo] Goal typed_succ_full_from_2_call_test_requires : Valid
+[wp] [Alt-Ergo] Goal typed_fail_cell_before_call_test_requires : Unsuccess
+[wp] [Alt-Ergo] Goal typed_fail_too_long_call_test_requires : Unsuccess
+[wp] [Alt-Ergo] Goal typed_fail_too_long_from_1_call_test_requires : Unsuccess
+[wp] [Alt-Ergo] Goal typed_fail_too_long_from_2_call_test_requires : Unsuccess
+[wp] [Alt-Ergo] Goal typed_fail_cell_after_end_call_test_requires : Unsuccess
+[wp] [Alt-Ergo] Goal typed_fail_partial_not_full_call_test_requires : Unsuccess
+[wp] Proved goals:    5 / 11
+  Qed:             1 
+  Alt-Ergo:        4  (unsuccess: 6)
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  succ_full_first_cell      1        -        1       100%
+  succ_full_full            -        1        1       100%
+  succ_full_from_1          -        1        1       100%
+  succ_from_1_from_1        -        1        1       100%
+  succ_full_from_2          -        1        1       100%
+  fail_cell_before          -        -        1       0.0%
+  fail_too_long             -        -        1       0.0%
+  fail_too_long_from_1      -        -        1       0.0%
+  fail_too_long_from_2      -        -        1       0.0%
+  fail_cell_after_end       -        -        1       0.0%
+  fail_partial_not_full     -        -        1       0.0%
+------------------------------------------------------------