aboutsummaryrefslogtreecommitdiffstats
path: root/riscV/Asm.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 /riscV/Asm.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 'riscV/Asm.v')
-rw-r--r--riscV/Asm.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/riscV/Asm.v b/riscV/Asm.v
index a47573a2..cbe3476a 100644
--- a/riscV/Asm.v
+++ b/riscV/Asm.v
@@ -751,7 +751,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
| Pj_l l =>
goto_label f l rs m
| Pj_s s sg =>
- Next (rs#PC <- (Genv.symbol_address ge s Ptrofs.zero)) m
+ Next (rs#PC <- (Genv.symbol_address ge s Ptrofs.zero) #X31 <- Vundef) m
| Pj_r r sg =>
Next (rs#PC <- (rs#r)) m
| Pjal_s s sg =>