From ce7013f94c97b0e46da03c97812b38df001fbc9d Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 15 Jan 2018 10:28:40 +0100 Subject: Use Ptrofs.repr instead of Int.repr for Init_addrof. (#51) This should fix issue 216 and also allows it to print 64 bit offsets. --- exportclight/ExportClight.ml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) (limited to 'exportclight') diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml index f5b8150d..6f5e3cdc 100644 --- a/exportclight/ExportClight.ml +++ b/exportclight/ExportClight.ml @@ -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 @@ -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); -- cgit From 2b598161e216402db6fe3780f1a00d7802bccb21 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 15 Jan 2018 10:30:11 +0100 Subject: Added type annotations for exported program. (#50) Added types for global_definitions in order to avoid problems with implicit parameters. This should fix issue 215 --- exportclight/ExportClight.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'exportclight') diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml index 6f5e3cdc..1b1402c3 100644 --- a/exportclight/ExportClight.ml +++ b/exportclight/ExportClight.ml @@ -555,10 +555,10 @@ let print_program p prog = fprintf p "Definition composites : list composite_definition :=@ "; print_list print_composite_definition p prog.prog_types; fprintf p ".@ @ "; - fprintf p "Definition global_definitions :=@ "; + fprintf p "Definition global_definitions : list (ident * globdef fundef type) :=@ "; print_list print_ident_globdef p prog.Ctypes.prog_defs; fprintf p ".@ @ "; - fprintf p "Definition public_idents :=@ "; + fprintf p "Definition public_idents : list ident :=@ "; print_list ident p prog.Ctypes.prog_public; fprintf p ".@ @ "; fprintf p "Definition prog : Clight.program := @ "; -- cgit