diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2018-03-08 16:36:16 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2018-03-08 16:36:16 +0100 |
| commit | bf21c2c43629ca47a2a34c47a01c4525a69a2ca6 (patch) | |
| tree | c00bd279c2be10fe5503f90217715d28b54f3e1e /riscV/TargetPrinter.ml | |
| parent | 355c79ae4ffe9a0669c06d7a3a3ce1eb86ccc5fb (diff) | |
| download | compcert-kvx-bf21c2c43629ca47a2a34c47a01c4525a69a2ca6.tar.gz compcert-kvx-bf21c2c43629ca47a2a34c47a01c4525a69a2ca6.zip | |
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
Diffstat (limited to 'riscV/TargetPrinter.ml')
| -rw-r--r-- | riscV/TargetPrinter.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml index 72b38bcd..e3fbfe36 100644 --- a/riscV/TargetPrinter.ml +++ b/riscV/TargetPrinter.ml @@ -568,11 +568,11 @@ module Target : TARGET = begin match ef with | EF_annot(kind,txt, targs) -> begin match (P.to_int kind) with - | 1 -> let annot = annot_text preg_annot "sp" (camlstring_of_coqstring txt) args in + | 1 -> let annot = annot_text preg_annot "x2" (camlstring_of_coqstring txt) args in fprintf oc "%s annotation: %S\n" comment annot | 2 -> let lbl = new_label () in fprintf oc "%a: " label lbl; - add_ais_annot lbl preg_annot "sp" (camlstring_of_coqstring txt) args + add_ais_annot lbl preg_annot "x2" (camlstring_of_coqstring txt) args | _ -> assert false end | EF_debug(kind, txt, targs) -> |