diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-06-01 11:05:15 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-06-01 11:05:15 +0200 |
| commit | 18859319b1daee0abb32bbc4e89ec5865a6fe082 (patch) | |
| tree | d50056bf5867a7d6b0144a098b18f929e2b90888 /exportclight | |
| parent | 0eba6f63b6bc458d856e477f6f8ec6b78ef78c58 (diff) | |
| download | compcert-kvx-18859319b1daee0abb32bbc4e89ec5865a6fe082.tar.gz compcert-kvx-18859319b1daee0abb32bbc4e89ec5865a6fe082.zip | |
clightgen -short-idents : do not use $"xxx" notation ever
In the original code, collisions could occur: an identifier could
be numbered with a number that happens to be equal to its canonical
encoding. This was harmless but confusing.
Closes: #358
Diffstat (limited to 'exportclight')
| -rw-r--r-- | exportclight/ExportClight.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml index 87956b58..96947545 100644 --- a/exportclight/ExportClight.ml +++ b/exportclight/ExportClight.ml @@ -81,7 +81,7 @@ let define_idents p = string_of_atom (fun (id, name) -> try - if id = pos_of_string name then + if !use_canonical_atoms && id = pos_of_string name then fprintf p "Definition _%s : ident := $\"%s\".@ " (sanitize name) name else |