string_of_ident

[andrew-appel]

With the new ident_of_string defined in exportclight/Clightdefs.v, some users may find it helpful to have string_of_ident as well as this lemma:

Lemma string_of_ident_of_string: forall s, string_of_ident (ident_of_string s) = s.

I hereby contribute the attached definitions and proofs into the open-source portion of CompCert, with the recommendation that they be added to Clightdefs.v.

If you don't want them, just let me know, and I will add them to VST instead.

string_of_ident.txt

[xavierleroy]

Yes, I like the idea of having string_of_ident in Clightdefs.v. I think we can do better than the 256-case matching for the "uncommon character" case. Give me a bit of time to look into this.

[xavierleroy]

I merged a variation on @andrew-appel 's code in commit 6aeb645.