[wp] suppress useless code

src/plugins/wp/cfgAnnot.ml

@@ -295,7 +295,7 @@ module CodeAssertions = WpContext.StaticGenerator(CodeKey)
       type data = code_assertions
       let name = "Wp.CfgAnnot.CodeAssertions"
       let compile (kf,stmt) =
-        let labels = NormAtLabels.labels_assert_before ~kf stmt in
+        let labels = NormAtLabels.labels_assert ~kf stmt in
         let normalize_pred p = NormAtLabels.preproc_annot labels p in
         reverse_code_assertions @@
         Annotations.fold_code_annot

src/plugins/wp/normAtLabels.ml

@@ -181,15 +181,10 @@ let labels_stmt_assigns_l ~kf s l_post = function
 (* --- User Assertions in Functions Code                                  --- *)
 (* -------------------------------------------------------------------------- *)
 
-let labels_assert_before ~kf s = function
+let labels_assert ~kf s = function
   | BuiltinLabel Here -> Clabels.stmt s
   | l -> labels_fct ~kf ~at:s l
 
-let labels_assert_after ~kf s l_post = function
-  | BuiltinLabel Old -> Clabels.stmt s
-  | BuiltinLabel Here as l -> option l l_post
-  | l -> labels_fct ~kf ~at:s l
-
 let labels_loop s = function
   (* In invariant preservation/establishment, LoopCurrent is Here. *)
   | BuiltinLabel (Here | LoopCurrent) -> Clabels.here

src/plugins/wp/normAtLabels.mli

@@ -32,8 +32,7 @@ val labels_empty : label_mapping
 val labels_fct_pre : label_mapping
 val labels_fct_post : label_mapping
 val labels_fct_assigns : label_mapping
-val labels_assert_before : kf:kernel_function -> stmt -> label_mapping
-val labels_assert_after : kf:kernel_function -> stmt -> c_label option -> label_mapping
+val labels_assert : kf:kernel_function -> stmt -> label_mapping
 val labels_loop : stmt -> label_mapping
 val labels_stmt_pre : kf:kernel_function -> stmt -> label_mapping
 val labels_stmt_post : kf:kernel_function -> stmt -> label_mapping

src/plugins/wp/wpStrategy.ml

@@ -268,7 +268,7 @@ let add_prop_call_post acc kind called_kf bhv tkind ~assumes post =
 
 let add_prop_assert acc kind kf s ca p =
   let id = WpPropId.mk_assert_id kf s ca in
-  let labels = NormAtLabels.labels_assert_before ~kf s in
+  let labels = NormAtLabels.labels_assert ~kf s in
   let p = normalize id labels p in
   add_prop acc kind id p