Compile
signed char __stringlit_42[] = {-3, 0};
on ARM.
Get
__stringlit_42:
.ascii "\777777777777777777775\000"
which is incorrect.
(I do understand that variables prefixed with __ are reserved and the above code is incorrect. But there is no warning.)
Proposed fix
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -453,7 +453,7 @@ let string_of_init id =
let b = Buffer.create (List.length id) in
let add_init = function
| Init_int8 n ->
- let c = Int32.to_int (camlint_of_coqint n) in
+ let c = Int32.to_int (camlint_of_coqint n) land 0xFF in
if c >= 32 && c <= 126 && c <> Char.code '\"' && c <> Char.code '\\'
then Buffer.add_char b (Char.chr c)
else Buffer.add_string b (Printf.sprintf "\\%03o" c)
``