Incorrect printout of constant initializers in rare circumstances

[monniaux]

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)
``

[xavierleroy]

"Doctor, it hurts when I used reserved names!". I'm not going to add "so don't do that", because lots of code uses reserved names, esp. C standard libraries. Plus, matching on variable names is not nice. So, #579 proposes to mark globals introduced to hold string literals specially, and rely on this accurate information for printing initializers.

[monniaux]

But how about masking bytes using 0xFF? This sounds prudent if, for any reason, out of range values reached this pass.

[xavierleroy]

#579 fails (with an assertion failure) if the bytes are not in 0..255. With the new code, this should never happen, and it's better to fail than to silently generate a possibly wrong initializer.