Favor standard visitor mechanism for updating gotos

labels.ml was broken since quite some time.

src/plugins/e-acsl/label.ml

@@ -51,22 +51,11 @@ let move (vis:Visitor.generic_frama_c_visitor) ~old new_stmt =
       inherit Visitor.frama_c_inplace
       (* invariant of this method: [s = Cil.memo_stmt vis#behavior orig_stmt] *)
       method !vstmt_aux s = match s.skind, orig_stmt.skind with
-      | Goto(s_ref, loc), Goto(orig_ref, _) ->
-        if Cil_datatype.Stmt.equal !s_ref old then
-          if s_ref == orig_ref then
-            (* The memo_stmt and its origin [orig_stmt] contain a shared
-               reference because [orig_stmt] has not yet been visited by [vis]
-               (forward goto). Consequently, do not modify the ref directly but
-               replace the corresponding stmt in the memoisation table. When
-               [orig_stmt] will be visited, the visitor will automatically
-               substitute it with the updated stmt. *)
-            Cil.set_stmt vis#behavior
-              orig_stmt
-              { s with skind = Goto(ref new_stmt, loc) }
-          else
-            (* Backward goto: it has already been visited and there is no more
-               sharing. Directly update the reference. *)
-            s_ref := new_stmt;
+      | Goto(s_ref, _), Goto(orig_ref, _) ->
+        if Cil_datatype.Stmt.equal !s_ref old && s_ref != orig_ref then
+          (* Forward goto: it has already been visited and there is no more
+             sharing. Must update the reference. *)
+          s_ref := new_stmt;
         Cil.SkipChildren
       | _ -> Cil.DoChildren
       (* improve efficiency: skip childrens which cannot contain any label *)

src/plugins/e-acsl/visit.ml

@@ -623,6 +623,9 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
       in
       (* handle loop invariants *)
       let new_stmt, env, must_mv = Loops.preserve_invariant prj env kf stmt in
+      let orig = Cil.get_original_stmt self#behavior stmt in
+      Cil.set_orig_stmt self#behavior new_stmt orig;
+      Cil.set_stmt self#behavior orig new_stmt;
       let new_stmt, env =
         (* Remove local variables which scopes ended via goto/break/continue. *)
         let del_vars = Exit_points.delete_vars stmt in
@@ -708,13 +711,16 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
                 Env.Before
             in
             let post_block =
-              if post_block.blocals = [] then Cil.transient_block post_block
+              if post_block.blocals = [] && new_stmt.labels = []
+              then Cil.transient_block post_block
               else post_block
             in
             let res = Misc.mk_block prj new_stmt post_block in
             if not (Cil_datatype.Stmt.equal new_stmt res) then
               E_acsl_label.move (self :> Visitor.generic_frama_c_visitor)
                 new_stmt res;
+            Cil.set_stmt self#behavior orig res;
+            Cil.set_orig_stmt self#behavior res orig;
             res, env
           end else
             stmt, env