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

6 files changed, 17 insertions, 14 deletions

diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index 9d09fc1..d90d7b6 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -719,8 +719,8 @@ let print_init oc = function
       fprintf oc "	.quad	%Ld %s %.18g\n" (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 "	.word	%a\n" print_symb_ofs (symb, ofs)
 
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 3830ca7..4233af9 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -779,11 +779,12 @@ let convertInitializer env ty i =
 let convertGlobvar env (sto, id, ty, optinit) =
   let id' = intern_string id.name in
   let ty' = convertTyp env ty in 
+  let sz = Ctypes.sizeof ty' in
   let attr = Cutil.attributes_of_type env ty in
   let init' =
     match optinit with
     | None ->
-        if sto = C.Storage_extern then [] else [Init_space(Ctypes.sizeof ty')]
+        if sto = C.Storage_extern then [] else [Init_space sz]
     | Some i ->
         convertInitializer env ty i in
   let align =
@@ -792,6 +793,9 @@ let convertGlobvar env (sto, id, ty, optinit) =
     | _            -> Cutil.alignof env ty in
   let (section, near_access) =
     Sections.for_variable env id' ty (optinit <> None) in
+  if Z.gt sz (Z.of_uint64 0xFFFF_FFFFL) then
+    error (sprintf "Variable %s is too big (%s bytes)"
+                   id.name (Z.to_string sz));
   Hashtbl.add decl_atom id'
     { a_storage = sto;
       a_alignment = align;
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index 601869b..0074405 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)
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index f56c3f2..0d2d201 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -924,8 +924,8 @@ let print_init oc = function
                  (Int64.logand b 0xFFFFFFFFL)
                  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)
@@ -964,10 +964,10 @@ let print_var oc name v =
       end else begin
         let sz =
           match v.gvar_init with [Init_space sz] -> sz | _ -> assert false in
-        fprintf oc "	%s	%a, %ld, %d\n"
+        fprintf oc "	%s	%a, %s, %d\n"
           (if C2C.atom_is_static name then ".lcomm" else ".comm")
           symbol name
-          (camlint_of_coqint sz)
+          (Z.to_string sz)
           (1 lsl align)
       end
 
diff --git a/test/c/Makefile b/test/c/Makefile
index 2b445d2..f4d8f41 100644
--- a/test/c/Makefile
+++ b/test/c/Makefile
@@ -17,10 +17,10 @@ PROGS=fib integr qsort fft sha1 aes almabench lists \
 
 PROGS_INTERP=floats
 
-all_s: $(PROGS:%=%.s)
-
 all: $(PROGS:%=%.compcert)
 
+all_s: $(PROGS:%=%.s)
+
 all_gcc: $(PROGS:%=%.gcc)
 
 %.compcert: %.c $(CCOMP)
diff --git a/test/regression/Makefile b/test/regression/Makefile
index 0a9212d..31ea51b 100644
--- a/test/regression/Makefile
+++ b/test/regression/Makefile
@@ -22,10 +22,10 @@ EXTRAS=annot1 commaprec expr2 expr3 expr4 extern1 funct2 funptr1 init1 \
 # Test known to fail
 FAILURES=funct1 varargs1
 
-all_s: $(TESTS:%=%.s) $(EXTRAS:%=%.s)
-
 all: $(TESTS:%=%.compcert) $(EXTRAS:%=%.s)
 
+all_s: $(TESTS:%=%.s) $(EXTRAS:%=%.s)
+
 %.compcert: %.c $(CCOMP)
 	$(CCOMP) $(CCOMPFLAGS) -o $*.compcert $*.c $(LIBS)