Identifier names generated by clightgen produce syntax error

[akinanop]

Version 3.7 of clightgen produces names that cannot be compiled with Coq 8.11.2:

Definition _t'-1181243039470217951 : ident := -822504032%positive.

To reproduce:
git clone https://github.com/vlm/asn1c.git
clightgen asn1c/skeletons/BOOLEAN.c -I asn1c/skeletons/ -normalize -fstruct-passing -flongdouble -o BOOLEAN.v

Couldn't reproduce on smaller examples, I guess the issue comes up in big functions when many temporary variables are introduced.

BOOLEAN.v

[xavierleroy]

Thanks for the report. It looks like an unexpected consequence of the -normalize mode interaction between the -normalize mode and the -canonical-idents mode that was introduced in 3.7 , which in turns causes an integer overflow during printing. I'll investigate.

[xavierleroy]

The generation of temporaries with huge numbers was fixed in commit d5e332e. For good measure, the printing of temporaries with huge numbers was hardened in commit 361726e -- there was no reason to use fixed-precision integers and risk overflow there.

[vzaliva]

@letouzey Thanks for the fix! I understand this bug is affecting the current release. When do you think there will be an updated release with this fix? We need to decide if we should wait for an updated release in OPAM or to follow a master branch as a dependency.

[xavierleroy]

My Github name is @xavierleroy. There will be a release by the end of the year. In the meantime you can try to use clightgen -normalize -short-idents, which gives you the same behavior as with CompCert 3.6, and doesn't run into the overflow issue.