Revised handling of annotation statements, and more generally built-in functions, and more generally external functions

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1672 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 7 insertions, 4 deletions

diff --git a/backend/Reload.v b/backend/Reload.v
index 81b61998..0ad53e6e 100644
--- a/backend/Reload.v
+++ b/backend/Reload.v
@@ -236,10 +236,13 @@ Definition transf_instr
             (Ltailcall sig (inr _ id) :: k)
       end
   | LTLin.Lbuiltin ef args dst =>
-      let rargs := regs_for args in
-      let rdst := reg_for dst in
-      add_reloads args rargs
-        (Lbuiltin ef rargs rdst :: add_spill rdst dst k)
+      if ef_reloads ef then
+       (let rargs := regs_for args in
+        let rdst := reg_for dst in
+        add_reloads args rargs
+          (Lbuiltin ef rargs rdst :: add_spill rdst dst k))
+      else
+        Lannot ef args :: k
   | LTLin.Llabel lbl =>
       Llabel lbl :: k
   | LTLin.Lgoto lbl =>