diff options
Diffstat (limited to 'backend/PrintAsmaux.ml')
| -rw-r--r-- | backend/PrintAsmaux.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index ff276af1..09630e29 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -91,8 +91,8 @@ let elf_symbol oc symb = let elf_symbol_offset oc (symb, ofs) = elf_symbol oc symb; - let ofs = camlint_of_coqint ofs in - if ofs <> 0l then fprintf oc " + %ld" ofs + let ofs = camlint64_of_ptrofs ofs in + if ofs <> 0L then fprintf oc " + %Ld" ofs (* Functions for fun and var info *) let elf_print_fun_info oc name = @@ -142,6 +142,9 @@ let coqint oc n = let coqint64 oc n = fprintf oc "%Ld" (camlint64_of_coqint n) +let ptrofs oc n = + fprintf oc "%Ld" (camlint64_of_ptrofs n) + (** Programmer-supplied annotations (__builtin_annot). *) let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*" |