diff options
Diffstat (limited to 'riscV/Asm.v')
| -rw-r--r-- | riscV/Asm.v | 2 |
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 => |