Skip to content

Commit

Permalink
Use Ptrofs.repr instead of Int.repr for Init_addrof. (#51)
Browse files Browse the repository at this point in the history
This should fix issue 216 and also allows it to print 64 bit offsets.
  • Loading branch information
bschommer authored and xavierleroy committed Jan 15, 2018
1 parent 879ba46 commit ce7013f
Showing 1 changed file with 7 additions and 1 deletion.
8 changes: 7 additions & 1 deletion exportclight/ExportClight.ml
Original file line number Diff line number Diff line change
Expand Up @@ -109,6 +109,12 @@ let coqint p n =
then fprintf p "(Int.repr %ld)" n
else fprintf p "(Int.repr (%ld))" n

let coqptrofs p n =
let s = Z.to_string n in
if Z.ge n Z.zero
then fprintf p "(Ptrofs.repr %s)" s
else fprintf p "(Ptrofs.repr (%s))" s

let coqint64 p n =
let n = camlint64_of_coqint n in
if n >= 0L
Expand Down Expand Up @@ -393,7 +399,7 @@ let init_data p = function
| Init_float32 n -> fprintf p "Init_float32 %a" coqsingle n
| Init_float64 n -> fprintf p "Init_float64 %a" coqfloat n
| Init_space n -> fprintf p "Init_space %ld" (Z.to_int32 n)
| Init_addrof(id,ofs) -> fprintf p "Init_addrof %a %a" ident id coqint ofs
| Init_addrof(id,ofs) -> fprintf p "Init_addrof %a %a" ident id coqptrofs ofs

let print_variable p (id, v) =
fprintf p "Definition v_%s := {|@ " (extern_atom id);
Expand Down

0 comments on commit ce7013f

Please sign in to comment.