diff options
Diffstat (limited to 'x86')
| -rw-r--r-- | x86/TargetPrinter.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml index b5aeefae..4a576df3 100644 --- a/x86/TargetPrinter.ml +++ b/x86/TargetPrinter.ml @@ -13,7 +13,6 @@ (* Printing x86-64 assembly code in asm syntax *) open Printf -open !Datatypes open Camlcoq open Sections open AST @@ -169,7 +168,7 @@ module MacOS_System : SYSTEM = if i then ".const" else "COMM" | Section_string -> ".const" | Section_literal -> ".literal8" - | Section_jumptable -> ".const" + | Section_jumptable -> ".text" (* needed in 64 bits, not a problem in 32 bits *) | Section_user(s, wr, ex) -> sprintf ".section \"%s\", %s, %s" (if wr then "__DATA" else "__TEXT") s @@ -244,9 +243,9 @@ module Target(System: SYSTEM):TARGET = let addressing_gen ireg oc (Addrmode(base, shift, cst)) = begin match cst with - | Coq_inl n -> + | Datatypes.Coq_inl n -> fprintf oc "%s" (Z.to_string n) - | Coq_inr(id, ofs) -> + | Datatypes.Coq_inr(id, ofs) -> if Archi.ptr64 then begin (* RIP-relative addressing *) let ofs' = Z.to_int64 ofs in |