[Kernel] Status_by_call changes node after visit for replacement

src/kernel_services/ast_data/statuses_by_call.ml

@@ -111,23 +111,27 @@ let replacement_visitor ~arguments = object (self)
     | TVar { lv_origin = Some vinfo } when vinfo.vformal ->
       if under_label then raise Non_Transposable;
       begin
-        let new_term = replace_formal_by_concrete vinfo arguments in
-        let add_offset lv = TLval (Logic_const.addTermOffsetLval t_offset lv) in
-        match new_term.term_node with
-        | TLval lv -> Cil.ChangeDoChildrenPost (add_offset lv, fun x -> x)
-        | _ ->
-          if t_offset = TNoOffset
-          then Cil.ChangeTo new_term.term_node
-          else
-            let ltyp = new_term.term_type in
-            let tmp_lvar = Cil.make_temp_logic_var ltyp in
-            let tmp_linfo =
-              { l_var_info = tmp_lvar; l_body = LBterm new_term;
-                l_type = None; l_tparams = []; l_labels = []; l_profile = [];  }
-            in
-            let lval_node = TLval (TVar tmp_lvar, t_offset) in
-            let lval_term = Tlet (tmp_linfo, Logic_const.term lval_node ltyp) in
-            Cil.ChangeDoChildrenPost (lval_term, fun x -> x)
+        let post_replace _ =
+          let new_term = replace_formal_by_concrete vinfo arguments in
+          let add_offset lv =
+            TLval (Logic_const.addTermOffsetLval t_offset lv)
+          in
+          match new_term.term_node with
+          | TLval lv -> add_offset lv
+          | node ->
+            if t_offset = TNoOffset then node
+            else
+              let ltyp = new_term.term_type in
+              let tmp_lvar = Cil.make_temp_logic_var ltyp in
+              let tmp_linfo =
+                { l_var_info = tmp_lvar; l_body = LBterm new_term;
+                  l_type = None; l_tparams = []; l_labels = [];
+                  l_profile = []; }
+              in
+              let lval_node = TLval (TVar tmp_lvar, t_offset) in
+              Tlet (tmp_linfo, Logic_const.term lval_node ltyp)
+        in
+        Cil.DoChildrenPost post_replace
       end
     | _ -> Cil.DoChildren
 
@@ -149,8 +153,7 @@ let replacement_visitor ~arguments = object (self)
     | _ -> Cil.DoChildren
 
   method! vlogic_label = function
-    | BuiltinLabel Pre ->
-      Cil.ChangeDoChildrenPost (Logic_const.here_label, fun x -> x)
+    | BuiltinLabel Pre -> Cil.DoChildrenPost (fun _ -> Logic_const.here_label)
     | _ -> Cil.DoChildren
 end