Add RA to the lsit of calee_saved registers.

It seems to avoid using RA as the return address storage AND the return value in the same function.
jasmin-lang · Oct 8, 2024 · 86effc3 · 86effc3
1 parent 582b3ca
commit 86effc3
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/proofs/compiler/riscv_decl.v b/proofs/compiler/riscv_decl.v
@@ -184,7 +184,7 @@ Instance riscv_decl : arch_decl register register_ext xregister rflag condt :=
      To be on the safe side, GP and TP (thread pointer) are marked as callee-saved. *)
   Definition riscv_linux_call_conv : calling_convention :=
   {| callee_saved :=
-      map ARReg [:: SP; GP; TP; X8; X9; X18; X19; X20; X21; X22; X23; X24; X25; X26; X27 ]
+   map ARReg [:: SP; RA; GP; TP; X8; X9; X18; X19; X20; X21; X22; X23; X24; X25; X26; X27 ]
    ; callee_saved_not_bool := erefl true
    ; call_reg_args  := [:: X10; X11; X12; X13; X14; X15; X16; X17 ]
    ; call_xreg_args := [::]