aboutsummaryrefslogtreecommitdiffstats
path: root/riscV/TargetPrinter.ml
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/TargetPrinter.ml
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/TargetPrinter.ml')
-rw-r--r--riscV/TargetPrinter.ml4
1 files changed, 1 insertions, 3 deletions
diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml
index d8137f84..366dc02e 100644
--- a/riscV/TargetPrinter.ml
+++ b/riscV/TargetPrinter.ml
@@ -315,12 +315,10 @@ module Target : TARGET =
fprintf oc " sra %a, %a, %a\n" ireg rd ireg0 rs1 ireg0 rs2
(* Unconditional jumps. Links are always to X1/RA. *)
- (* TODO: fix up arguments for calls to variadics, to move *)
- (* floating point arguments to integer registers. How? *)
| Pj_l(l) ->
fprintf oc " j %a\n" print_label l
| Pj_s(s, sg) ->
- fprintf oc " j %a\n" symbol s
+ fprintf oc " jump %a, x31\n" symbol s
| Pj_r(r, sg) ->
fprintf oc " jr %a\n" ireg r
| Pjal_s(s, sg) ->