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. --- cfrontend/PrintCsyntax.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'cfrontend/PrintCsyntax.ml') diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index 6e016cb3..3a44796c 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -466,7 +466,7 @@ let print_init p = function | Init_int64 n -> fprintf p "%LdLL" (camlint64_of_coqint n) | Init_float32 n -> fprintf p "%.15F" (camlfloat_of_coqfloat n) | Init_float64 n -> fprintf p "%.15F" (camlfloat_of_coqfloat n) - | Init_space n -> fprintf p "/* skip %ld */@ " (camlint_of_coqint n) + | Init_space n -> fprintf p "/* skip %s */@ " (Z.to_string n) | Init_addrof(symb, ofs) -> let ofs = camlint_of_coqint ofs in if ofs = 0l -- cgit