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 /powerpc/PrintAsm.ml | |
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
Diffstat (limited to 'powerpc/PrintAsm.ml')
-rw-r--r-- | powerpc/PrintAsm.ml | 8 |
1 files changed, 4 insertions, 4 deletions
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 |