Skip to content

Commit bf21c2c

Browse files
committed
Print x2 for riscV stack pointer.
x2 is the stack pointer of the riscV, both sp and x2 are supported but to be safe use x2 in annotations. Bug 23176
1 parent 355c79a commit bf21c2c

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

Diff for: riscV/TargetPrinter.ml

+2-2
Original file line numberDiff line numberDiff line change
@@ -568,11 +568,11 @@ module Target : TARGET =
568568
begin match ef with
569569
| EF_annot(kind,txt, targs) ->
570570
begin match (P.to_int kind) with
571-
| 1 -> let annot = annot_text preg_annot "sp" (camlstring_of_coqstring txt) args in
571+
| 1 -> let annot = annot_text preg_annot "x2" (camlstring_of_coqstring txt) args in
572572
fprintf oc "%s annotation: %S\n" comment annot
573573
| 2 -> let lbl = new_label () in
574574
fprintf oc "%a: " label lbl;
575-
add_ais_annot lbl preg_annot "sp" (camlstring_of_coqstring txt) args
575+
add_ais_annot lbl preg_annot "x2" (camlstring_of_coqstring txt) args
576576
| _ -> assert false
577577
end
578578
| EF_debug(kind, txt, targs) ->

0 commit comments

Comments
 (0)