[wp] Simplifies loop computation

src/plugins/wp/cfgCalculus.ml

@@ -232,22 +232,16 @@ struct
 
   (* Compute loops *)
   and loop env a s (lc : CfgAnnot.loop_contract) : W.t_prop =
-    let loop_current = Clabels.loop_current s in
-    let established =
-      W.label env.we None loop_current @@
-      List.fold_right (prove_property env) lc.loop_established W.empty in
-    let presersed =
-      List.fold_right (use_assigns env) lc.loop_assigns @@
-      W.label env.we None loop_current @@
-      List.fold_right (use_property env) lc.loop_invariants @@
-      List.fold_right (prove_property env) lc.loop_smoke @@
-      let q =
-        List.fold_right (prove_property env) lc.loop_preserved @@
-        List.fold_right (prove_assigns env) lc.loop_assigns @@
-        W.empty in
-      ( Vhash.replace env.wp a (Some q) ; successors env a )
-    in
-    W.merge env.we established presersed
+    List.fold_right (prove_property env) lc.loop_established @@
+    List.fold_right (use_assigns env) lc.loop_assigns @@
+    W.label env.we None (Clabels.loop_current s) @@
+    List.fold_right (use_property env) lc.loop_invariants @@
+    List.fold_right (prove_property env) lc.loop_smoke @@
+    let q =
+      List.fold_right (prove_property env) lc.loop_preserved @@
+      List.fold_right (prove_assigns env) lc.loop_assigns @@
+      W.empty in
+    ( Vhash.replace env.wp a (Some q) ; successors env a )
 
   (* Merge transitions *)
   and successors env (a : vertex) = transitions env (env.succ a)

src/plugins/wp/normAtLabels.ml

@@ -121,6 +121,8 @@ let labels_fct ?kf ?at l =
   | BuiltinLabel Pre -> Clabels.pre
   | StmtLabel at -> Clabels.stmt !at
   | BuiltinLabel LoopEntry -> Clabels.loop_entry (enclosing_loop ?kf ?at l)
+  (* Labels fct is not used to label invariant establishment/preservation,
+     thus, contrary to what is done in [labels_loop], Current is not Here. *)
   | BuiltinLabel LoopCurrent -> Clabels.loop_current (enclosing_loop ?kf ?at l)
   | _ -> raise (LabelError l)
 
@@ -189,6 +191,7 @@ let labels_assert_after ~kf s l_post = function
   | l -> labels_fct ~kf ~at:s l
 
 let labels_loop s = function
+  (* In invariant preservation/establishment, LoopCurrent is Here. *)
   | BuiltinLabel (Here | LoopCurrent) -> Clabels.here
   | BuiltinLabel LoopEntry -> Clabels.loop_entry s
   | FormalLabel wplabel -> Clabels.formal wplabel