Fixes issues in updating labels and gotos during instrumentation

Label.move must compare goto targets to the statement in the original
AST, not its copy. Furthermore moving labels must only be done if we
are about to change the target of the gotos, not if we use the
statement as generated by the plain visitor.

src/plugins/e-acsl/label.ml

@@ -44,6 +44,7 @@ let move (vis:Visitor.generic_frama_c_visitor) ~old new_stmt =
   | _ :: _ ->
     old.labels <- [];
     new_stmt.labels <- labels @ new_stmt.labels;
+    let old = Cil.get_original_stmt vis#behavior old in
     Labeled_stmts.add old new_stmt;
     (* update the gotos of the function jumping to one of the labels *)
     let o orig_stmt = object

src/plugins/e-acsl/visit.ml

@@ -678,10 +678,12 @@ you must call function `%s' and `__e_acsl_memory_clean by yourself.@]"
                 b.bstmts <- List.rev l @ delete_stmts
             end;
             let new_stmt = Misc.mk_block prj stmt b in
-            (* move the labels of the return to the new block in order to
-               evaluate the postcondition when jumping to them. *)
-            E_acsl_label.move
-              (self :> Visitor.generic_frama_c_visitor) stmt new_stmt;
+            if not (Cil_datatype.Stmt.equal stmt new_stmt) then begin
+              (* move the labels of the return to the new block in order to
+                 evaluate the postcondition when jumping to them. *)
+              E_acsl_label.move
+                (self :> Visitor.generic_frama_c_visitor) stmt new_stmt
+            end;
             new_stmt, env
           else
             stmt, env