diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-09-17 19:44:22 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-09-17 19:44:22 +0200 |
| commit | f1637021cd51505796e878a21d1b30df0b42e236 (patch) | |
| tree | 9d87ecd26f560cee6be1f0a1fe410d4d6d0f4609 /.gitattributes | |
| parent | e1725209b2b4401adc63ce5238fa5db7c134609c (diff) | |
| download | compcert-kvx-f1637021cd51505796e878a21d1b30df0b42e236.tar.gz compcert-kvx-f1637021cd51505796e878a21d1b30df0b42e236.zip | |
Model GPR0 in isel (#199)
If the first argument to `isel` is GPR0, it reads as the constant 0.
This cannot occur in code generated by CompCert, due to the fact that
GPR0 is not available as register for register allocation. However the
assembler semantics should be as close as possible to the actual
hardware.
Diffstat (limited to '.gitattributes')
0 files changed, 0 insertions, 0 deletions