Merge tag 'v3.4' into mppa_k1c

Conflicts:
	.gitignore

1 files changed, 32 insertions, 0 deletions

diff --git a/backend/Asmexpandaux.ml b/backend/Asmexpandaux.ml
index 62c4a702..0f666a65 100644
--- a/backend/Asmexpandaux.ml
+++ b/backend/Asmexpandaux.ml
@@ -97,6 +97,16 @@ let translate_annot sp preg_to_dwarf annot =
   | [] -> None
   | a::_ -> aux a)
 
+let builtin_nop =
+  let signature ={sig_args = []; sig_res = None; sig_cc = cc_default} in
+  let name = coqstring_of_camlstring "__builtin_nop" in
+  Pbuiltin(EF_builtin(name,signature),[],BR_none)
+
+let rec lbl_follows = function
+  | Pbuiltin (EF_debug _, _, _):: rest ->
+    lbl_follows rest
+  | Plabel _ :: _ -> true
+  | _ -> false
 
 let expand_debug id sp preg simple l =
   let get_lbl = function
@@ -144,6 +154,11 @@ let expand_debug id sp preg simple l =
           | _ ->
               aux None scopes rest
         end
+    | (Pbuiltin(EF_annot (kind, _, _),_,_) as annot)::rest ->
+      simple annot;
+      if P.to_int kind = 2 && lbl_follows rest then
+        simple builtin_nop;
+      aux None scopes rest
     | (Plabel lbl)::rest -> simple (Plabel lbl); aux (Some lbl) scopes rest
     | i::rest -> simple i; aux None scopes rest in
   (* We need to move all closing debug annotations before the last real statement *)
@@ -157,3 +172,20 @@ let expand_debug id sp preg simple l =
     | b::rest -> List.rev ((List.rev (b::bcc)@List.rev acc)@rest) (* We found the first non debug location *)
     | [] -> List.rev acc (* This actually can never happen *) in
   aux None [] (move_debug [] [] (List.rev l))
+
+let expand_simple simple l =
+  let rec aux = function
+   | (Pbuiltin(EF_annot (kind, _, _),_,_) as annot)::rest ->
+     simple annot;
+     if P.to_int kind = 2 && lbl_follows rest then
+       simple builtin_nop;
+     aux rest
+   | i::rest -> simple i; aux rest
+   | [] -> () in
+  aux l
+
+let expand id sp preg simple l =
+  if !Clflags.option_g then
+    expand_debug id sp preg simple l
+  else
+    expand_simple simple l