aboutsummaryrefslogtreecommitdiffstats
path: root/common/Switch.v
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@college-de-france.fr>2022-06-24 18:55:21 +0200
committerXavier Leroy <xavier.leroy@college-de-france.fr>2022-06-24 19:22:27 +0200
commita34adc8e005447e7fa44ca3b71db35ceb7facb4c (patch)
treed1c7308d30254d39694877fceaccb8a168a2660a /common/Switch.v
parent44a668fbd81a587a17b680bebecf016519915a69 (diff)
downloadcompcert-a34adc8e005447e7fa44ca3b71db35ceb7facb4c.tar.gz
compcert-a34adc8e005447e7fa44ca3b71db35ceb7facb4c.zip
Expand "j_s symb" to "jump symb, x31" assembly pseudo-instruction
As suggested by Léo Gourdin in #437. The previous expansion as a plain "j" instruction fails when the jump offset is too large to be represented (issue #436). Fixes: #436 Closes: #437
Diffstat (limited to 'common/Switch.v')
0 files changed, 0 insertions, 0 deletions