Repository navigation
Incorrect printout of constant initializers in rare circumstances #577
Description
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)
``
Activity
xavierleroy commentedon Mar 24, 2026
"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 commentedon Mar 24, 2026
But how about masking bytes using 0xFF? This sounds prudent if, for any reason, out of range values reached this pass.
xavierleroy commentedon Mar 24, 2026
#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.