From 8f2e818c444363e29675d569ceaac48203f9d006 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sat, 2 Feb 2013 11:32:47 +0000
Subject: Errors for excessively large global variables or stack frames. test/:
 update Makefiles so that "all" is the default target.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2107 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 ia32/PrintAsm.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'ia32')

diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index 601869b8..00744055 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -204,7 +204,6 @@ let sp_adjustment sz =
   let sz = int32_align sz stack_alignment in
   (* The top 4 bytes have already been allocated by the "call" instruction. *)
   let sz = Int32.sub sz 4l in
-  assert (sz >= 0l);
   sz
 
 (* Base-2 log of a Caml integer *)
@@ -787,8 +786,8 @@ let print_init oc = function
 	(camlint64_of_coqint (Floats.Float.bits_of_double n))
 	comment (camlfloat_of_coqfloat n)
   | Init_space n ->
-      let n = Z.to_int32 n in
-      if n > 0l then fprintf oc "	.space	%ld\n" n
+      if Z.gt n Z.zero then
+        fprintf oc "	.space	%s\n" (Z.to_string n)
   | Init_addrof(symb, ofs) ->
       fprintf oc "	.long	%a\n" 
                  symbol_offset (symb, camlint_of_coqint ofs)
-- 
cgit