diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-02-02 11:32:47 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-02-02 11:32:47 +0000 |
commit | 8f2e818c444363e29675d569ceaac48203f9d006 (patch) | |
tree | 290e1b86688466b686dad14d644c3d57839c5ba9 | |
parent | d2cf6277ac179c9e8432d4c11a79e9f906a19bbc (diff) | |
download | compcert-8f2e818c444363e29675d569ceaac48203f9d006.tar.gz compcert-8f2e818c444363e29675d569ceaac48203f9d006.zip |
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
-rw-r--r-- | arm/PrintAsm.ml | 4 | ||||
-rw-r--r-- | cfrontend/C2C.ml | 6 | ||||
-rw-r--r-- | ia32/PrintAsm.ml | 5 | ||||
-rw-r--r-- | powerpc/PrintAsm.ml | 8 | ||||
-rw-r--r-- | test/c/Makefile | 4 | ||||
-rw-r--r-- | test/regression/Makefile | 4 |
6 files changed, 17 insertions, 14 deletions
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index 9d09fc19..d90d7b64 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 3830ca7b..4233af99 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 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) diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index f56c3f22..0d2d201e 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 2b445d22..f4d8f419 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 0a9212d9..31ea51b3 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) |