Support for indirect symbols under MacOS X (final).

Remove stdio hack in runtime/


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

1 files changed, 11 insertions, 0 deletions

diff --git a/backend/Constprop.v b/backend/Constprop.v
index bc6a647..19e5d1a 100644
--- a/backend/Constprop.v
+++ b/backend/Constprop.v
@@ -251,6 +251,17 @@ Definition transf_ros (app: D.t) (ros: reg + ident) : reg + ident :=
   | inr s => ros
   end.
 
+Parameter generate_float_constants : unit -> bool.
+
+Definition const_for_result (a: approx) : option operation :=
+  match a with
+  | I n => Some(Ointconst n)
+  | F n => if generate_float_constants tt then Some(Ofloatconst n) else None
+  | G symb ofs => Some(Oaddrsymbol symb ofs)
+  | S ofs => Some(Oaddrstack ofs)
+  | _ => None
+  end.
+
 Definition transf_instr (gapp: global_approx) (app: D.t) (instr: instruction) :=
   match instr with
   | Iop op args res s =>