diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-12-07 17:39:27 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-12-07 17:39:27 +0100 |
| commit | f4b66ff05ab0affb47ebf390502cba5c277caea3 (patch) | |
| tree | 4dbeac244b5f004f529be9f2111d85b7fb31dc7d /.gitattributes | |
| parent | a79f0f99831aa0b0742bf7cce459cc9353bd7cd0 (diff) | |
| download | compcert-kvx-f4b66ff05ab0affb47ebf390502cba5c277caea3.tar.gz compcert-kvx-f4b66ff05ab0affb47ebf390502cba5c277caea3.zip | |
Enforce evaluation order in IRC.add_interf and IRC.add_pref
As written previously, OCaml can evaluate `nodeOfVar g v1` and
`nodeOfVar g v2` in any order. Consequently, `v1` and `v2` can be
entered in the `varTable` hash table in different order. This can
result in different (but equally valid) register allocations.
It's better to enforce one evaluation order for the sake of
reproducible compilations when the OCaml version changes.
Diffstat (limited to '.gitattributes')
0 files changed, 0 insertions, 0 deletions