From 4d7a6709946a0c30e932c00405252b42e348eb64 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 13 Mar 2018 14:04:49 +0100 Subject: Print size argument of Init_space as Z not as int32 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Init_space has an argument of type Z and it can exceed the range of a 32-bit integer. Reported by Frédéric Besson. --- exportclight/ExportClight.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'exportclight') diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml index 1b1402c3..1ae78c15 100644 --- a/exportclight/ExportClight.ml +++ b/exportclight/ExportClight.ml @@ -398,7 +398,7 @@ let init_data p = function | Init_int64 n -> fprintf p "Init_int64 %a" coqint64 n | 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_space n -> fprintf p "Init_space %a" coqZ n | Init_addrof(id,ofs) -> fprintf p "Init_addrof %a %a" ident id coqptrofs ofs let print_variable p (id, v) = -- cgit