Merge branch 'feature/wp/const-deps' into 'master'

[wp] Keep global const dependencies

Closes #695

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

src/plugins/wp/cfgInit.ml

@@ -26,22 +26,22 @@ module Make(W : Mcfg.S) =
 struct
 
   let compute_global_init wenv filter obj =
-    Globals.Vars.fold_in_file_order
+    Globals.Vars.fold_in_file_rev_order
       (fun var initinfo obj ->
+
          if var.vstorage = Extern then obj else
            let do_init = match filter with
              | `All -> true
              | `InitConst -> Cil.isGlobalInitConst var
            in if not do_init then obj
-           else
-             let old_loc = Cil.CurrentLoc.get () in
+           else let old_loc = Cil.CurrentLoc.get () in
              Cil.CurrentLoc.set var.vdecl ;
              let obj = W.init wenv var initinfo.init obj in
              Cil.CurrentLoc.set old_loc ; obj
       ) obj
 
   let process_global_const wenv obj =
-    Globals.Vars.fold_in_file_order
+    Globals.Vars.fold_in_file_rev_order
       (fun var _initinfo obj ->
          if Cil.isGlobalInitConst var
          then W.const wenv var obj

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

+static int const A = 1 ;
+static int const B = A+1 ;
+
+int main(void) {
+  //@ assert B == 2 ;
+  return 0;
+}

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

+# frama-c -wp [...]
+[kernel] Parsing global_const_dependencies.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function main
+------------------------------------------------------------
+
+Goal Assertion (file global_const_dependencies.i, line 5):
+Prove: true.
+
+------------------------------------------------------------

src/plugins/wp/tests/wp_acsl/oracle/init_value_mem.0.res.oracle

@@ -14,13 +14,13 @@ Assume {
   (* Heap *)
   Type: region(G_v_20) <= 0.
   (* Initializer *)
-  Init: (w.F1_St_a) = 1.
-  (* Initializer *)
-  Init: (w.F1_St_b) = 2.
-  (* Initializer *)
   Init: Mint_0[shiftfield_F1_St_a(a)] = 1.
   (* Initializer *)
   Init: Mint_0[shiftfield_F1_St_b(a)] = 2.
+  (* Initializer *)
+  Init: (w.F1_St_a) = 1.
+  (* Initializer *)
+  Init: (w.F1_St_b) = 2.
 }
 Prove: EqS1_St(a_1, w).
 
@@ -34,13 +34,13 @@ Assume {
   (* Heap *)
   Type: region(G_v_20) <= 0.
   (* Initializer *)
-  Init: (w.F1_St_a) = 1.
-  (* Initializer *)
-  Init: (w.F1_St_b) = 2.
-  (* Initializer *)
   Init: Mint_0[shiftfield_F1_St_a(a)] = 1.
   (* Initializer *)
   Init: Mint_0[shiftfield_F1_St_b(a)] = 2.
+  (* Initializer *)
+  Init: (w.F1_St_a) = 1.
+  (* Initializer *)
+  Init: (w.F1_St_b) = 2.
 }
 Prove: EqS1_St(a_1, w).
 

src/plugins/wp/tests/wp_acsl/oracle/init_value_mem.1.res.oracle

@@ -11,13 +11,13 @@ Goal Post-condition 'P' in 'main':
 Assume {
   Type: IsS1_St(v) /\ IsS1_St(w).
   (* Initializer *)
-  Init: (w.F1_St_a) = 1.
-  (* Initializer *)
-  Init: (w.F1_St_b) = 2.
-  (* Initializer *)
   Init: (v.F1_St_a) = 1.
   (* Initializer *)
   Init: (v.F1_St_b) = 2.
+  (* Initializer *)
+  Init: (w.F1_St_a) = 1.
+  (* Initializer *)
+  Init: (w.F1_St_b) = 2.
 }
 Prove: EqS1_St(v, w).
 

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

+# frama-c -wp [...]
+[kernel] Parsing global_const_dependencies.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] 1 goal scheduled
+[wp] [Qed] Goal typed_main_assert : Valid
+[wp] Proved goals:    1 / 1
+  Qed:             1
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  main                      1        -        1       100%
+------------------------------------------------------------

src/plugins/wp/tests/wp_store/oracle/struct.res.oracle

@@ -49,13 +49,13 @@ Assume {
   (* Heap *)
   Type: region(G_v_30) <= 0.
   (* Initializer *)
-  Init: (w.F2_St_a) = 1.
-  (* Initializer *)
-  Init: (w.F2_St_b) = 2.
-  (* Initializer *)
   Init: Mint_0[shiftfield_F2_St_a(a)] = 1.
   (* Initializer *)
   Init: Mint_0[shiftfield_F2_St_b(a)] = 2.
+  (* Initializer *)
+  Init: (w.F2_St_a) = 1.
+  (* Initializer *)
+  Init: (w.F2_St_b) = 2.
 }
 Prove: EqS2_St(a_1, w).
 
@@ -69,13 +69,13 @@ Assume {
   (* Heap *)
   Type: region(G_v_30) <= 0.
   (* Initializer *)
-  Init: (w.F2_St_a) = 1.
-  (* Initializer *)
-  Init: (w.F2_St_b) = 2.
-  (* Initializer *)
   Init: Mint_0[shiftfield_F2_St_a(a)] = 1.
   (* Initializer *)
   Init: Mint_0[shiftfield_F2_St_b(a)] = 2.
+  (* Initializer *)
+  Init: (w.F2_St_a) = 1.
+  (* Initializer *)
+  Init: (w.F2_St_b) = 2.
 }
 Prove: EqS2_St(a_1, w).
 

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

@@ -30,108 +30,6 @@ Assume {
   (* Goal *)
   When: (0 <= i) /\ (i <= 499).
   (* Initializer *)
-  Init: h2_0[0] = 0.
-  (* Initializer *)
-  Init: h2_0[1] = 1.
-  (* Initializer *)
-  Init: h2_0[2] = 2.
-  (* Initializer *)
-  Init: h2_0[3] = 3.
-  (* Initializer *)
-  Init: h2_0[4] = 4.
-  (* Initializer *)
-  Init: h2_0[5] = 5.
-  (* Initializer *)
-  Init: h2_0[6] = 6.
-  (* Initializer *)
-  Init: h2_0[7] = 7.
-  (* Initializer *)
-  Init: h2_0[8] = 8.
-  (* Initializer *)
-  Init: h2_0[9] = 9.
-  (* Initializer *)
-  Init: h2_0[10] = 10.
-  (* Initializer *)
-  Init: h2_0[11] = 11.
-  (* Initializer *)
-  Init: h2_0[12] = 12.
-  (* Initializer *)
-  Init: h2_0[13] = 13.
-  (* Initializer *)
-  Init: h2_0[14] = 14.
-  (* Initializer *)
-  Init: h2_0[15] = 15.
-  (* Initializer *)
-  Init: h2_0[16] = 16.
-  (* Initializer *)
-  Init: h2_0[17] = 17.
-  (* Initializer *)
-  Init: h2_0[18] = 18.
-  (* Initializer *)
-  Init: h2_0[19] = 19.
-  (* Initializer *)
-  Init: h2_0[20] = 20.
-  (* Initializer *)
-  Init: h2_0[21] = 21.
-  (* Initializer *)
-  Init: h2_0[22] = 22.
-  (* Initializer *)
-  Init: h2_0[23] = 23.
-  (* Initializer *)
-  Init: h2_0[24] = 24.
-  (* Initializer *)
-  Init: h2_0[25] = 25.
-  (* Initializer *)
-  Init: h2_0[26] = 26.
-  (* Initializer *)
-  Init: h2_0[27] = 27.
-  (* Initializer *)
-  Init: h2_0[28] = 28.
-  (* Initializer *)
-  Init: h2_0[29] = 29.
-  (* Initializer *)
-  Init: h2_0[30] = 30.
-  (* Initializer *)
-  Init: h2_0[31] = 31.
-  (* Initializer *)
-  Init: h2_0[32] = 32.
-  (* Initializer *)
-  Init: h2_0[33] = 33.
-  (* Initializer *)
-  Init: h2_0[34] = 34.
-  (* Initializer *)
-  Init: h2_0[35] = 35.
-  (* Initializer *)
-  Init: h2_0[36] = 36.
-  (* Initializer *)
-  Init: h2_0[37] = 37.
-  (* Initializer *)
-  Init: h2_0[38] = 38.
-  (* Initializer *)
-  Init: h2_0[39] = 39.
-  (* Initializer *)
-  Init: h2_0[40] = 40.
-  (* Initializer *)
-  Init: h2_0[41] = 41.
-  (* Initializer *)
-  Init: h2_0[42] = 42.
-  (* Initializer *)
-  Init: h2_0[43] = 43.
-  (* Initializer *)
-  Init: h2_0[44] = 44.
-  (* Initializer *)
-  Init: h2_0[45] = 45.
-  (* Initializer *)
-  Init: h2_0[46] = 46.
-  (* Initializer *)
-  Init: h2_0[47] = 47.
-  (* Initializer *)
-  Init: h2_0[48] = 48.
-  (* Initializer *)
-  Init: h2_0[49] = 49.
-  (* Initializer *)
-  Init: forall i_1 : Z. ((50 <= i_1) -> ((i_1 <= 499) -> (h2_0[i_1] = 0))).
-  (* Initializer *)
   Init: h1_0[0] = 0.
   (* Initializer *)
   Init: h1_0[1] = 1.
@@ -233,6 +131,108 @@ Assume {
   Init: h1_0[49] = 49.
   (* Initializer *)
   Init: forall i_1 : Z. ((50 <= i_1) -> ((i_1 <= 499) -> (h1_0[i_1] = 0))).
+  (* Initializer *)
+  Init: h2_0[0] = 0.
+  (* Initializer *)
+  Init: h2_0[1] = 1.
+  (* Initializer *)
+  Init: h2_0[2] = 2.
+  (* Initializer *)
+  Init: h2_0[3] = 3.
+  (* Initializer *)
+  Init: h2_0[4] = 4.
+  (* Initializer *)
+  Init: h2_0[5] = 5.
+  (* Initializer *)
+  Init: h2_0[6] = 6.
+  (* Initializer *)
+  Init: h2_0[7] = 7.
+  (* Initializer *)
+  Init: h2_0[8] = 8.
+  (* Initializer *)
+  Init: h2_0[9] = 9.
+  (* Initializer *)
+  Init: h2_0[10] = 10.
+  (* Initializer *)
+  Init: h2_0[11] = 11.
+  (* Initializer *)
+  Init: h2_0[12] = 12.
+  (* Initializer *)
+  Init: h2_0[13] = 13.
+  (* Initializer *)
+  Init: h2_0[14] = 14.
+  (* Initializer *)
+  Init: h2_0[15] = 15.
+  (* Initializer *)
+  Init: h2_0[16] = 16.
+  (* Initializer *)
+  Init: h2_0[17] = 17.
+  (* Initializer *)
+  Init: h2_0[18] = 18.
+  (* Initializer *)
+  Init: h2_0[19] = 19.
+  (* Initializer *)
+  Init: h2_0[20] = 20.
+  (* Initializer *)
+  Init: h2_0[21] = 21.
+  (* Initializer *)
+  Init: h2_0[22] = 22.
+  (* Initializer *)
+  Init: h2_0[23] = 23.
+  (* Initializer *)
+  Init: h2_0[24] = 24.
+  (* Initializer *)
+  Init: h2_0[25] = 25.
+  (* Initializer *)
+  Init: h2_0[26] = 26.
+  (* Initializer *)
+  Init: h2_0[27] = 27.
+  (* Initializer *)
+  Init: h2_0[28] = 28.
+  (* Initializer *)
+  Init: h2_0[29] = 29.
+  (* Initializer *)
+  Init: h2_0[30] = 30.
+  (* Initializer *)
+  Init: h2_0[31] = 31.
+  (* Initializer *)
+  Init: h2_0[32] = 32.
+  (* Initializer *)
+  Init: h2_0[33] = 33.
+  (* Initializer *)
+  Init: h2_0[34] = 34.
+  (* Initializer *)
+  Init: h2_0[35] = 35.
+  (* Initializer *)
+  Init: h2_0[36] = 36.
+  (* Initializer *)
+  Init: h2_0[37] = 37.
+  (* Initializer *)
+  Init: h2_0[38] = 38.
+  (* Initializer *)
+  Init: h2_0[39] = 39.
+  (* Initializer *)
+  Init: h2_0[40] = 40.
+  (* Initializer *)
+  Init: h2_0[41] = 41.
+  (* Initializer *)
+  Init: h2_0[42] = 42.
+  (* Initializer *)
+  Init: h2_0[43] = 43.
+  (* Initializer *)
+  Init: h2_0[44] = 44.
+  (* Initializer *)
+  Init: h2_0[45] = 45.
+  (* Initializer *)
+  Init: h2_0[46] = 46.
+  (* Initializer *)
+  Init: h2_0[47] = 47.
+  (* Initializer *)
+  Init: h2_0[48] = 48.
+  (* Initializer *)
+  Init: h2_0[49] = 49.
+  (* Initializer *)
+  Init: forall i_1 : Z. ((50 <= i_1) -> ((i_1 <= 499) -> (h2_0[i_1] = 0))).
 }
 Prove: h2_0[i] = h1_0[i].
 

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

@@ -24,8 +24,8 @@ Prove: Mint_0[shift_sint32(a, i)] = 0.
 ------------------------------------------------------------
 
 Goal Assertion (file array_initialized.c, line 185):
-Let a = global(K_h1_26).
-Let a_1 = global(K_h2_27).
+Let a = global(K_h2_27).
+Let a_1 = global(K_h1_26).
 Assume {
   (* Goal *)
   When: (0 <= i) /\ (i <= 499).
@@ -236,7 +236,7 @@ Assume {
   Init: forall i_1 : Z. ((50 <= i_1) -> ((i_1 <= 499) ->
       (Mint_0[shift_sint32(a, i_1)] = 0))).
 }
-Prove: Mint_0[shift_sint32(a_1, i)] = Mint_0[shift_sint32(a, i)].
+Prove: Mint_0[shift_sint32(a, i)] = Mint_0[shift_sint32(a_1, i)].
 
 ------------------------------------------------------------
 ------------------------------------------------------------