diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-10-25 11:05:43 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-10-25 11:05:43 +0200 |
| commit | cc264a58d6fb43cf7c8ae41d73726dfedc20f1d4 (patch) | |
| tree | 0d4518c19ae9412c934d61494b536a6274f1ed3e /arm/TargetPrinter.ml | |
| parent | 011d9ef9a964a676380bb45195418595108e274b (diff) | |
| download | compcert-kvx-cc264a58d6fb43cf7c8ae41d73726dfedc20f1d4.tar.gz compcert-kvx-cc264a58d6fb43cf7c8ae41d73726dfedc20f1d4.zip | |
Fix register name of ais printing and moved label function up.
Diffstat (limited to 'arm/TargetPrinter.ml')
| -rw-r--r-- | arm/TargetPrinter.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 67bc5d8b..7abd9074 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -43,6 +43,8 @@ struct (* Basic printing functions *) + let label = elf_label + let print_label oc lbl = elf_label oc (transl_label lbl) let comment = "@" @@ -728,8 +730,8 @@ struct begin match (P.to_int kind) with | 1 -> annot_text preg_annot "sp" (camlstring_of_coqstring txt) args | 2 -> let lbl = new_label () in - fprintf oc "%a: " elf_label lbl; - ais_annot_text lbl preg_annot "r1" (camlstring_of_coqstring txt) args + fprintf oc "%a: " label lbl; + ais_annot_text lbl preg_annot "sp" (camlstring_of_coqstring txt) args | _ -> assert false end in fprintf oc "%s annotation: %S\n" comment annot; @@ -884,8 +886,6 @@ struct let default_falignment = 4 - let label = elf_label - let new_label = new_label let address = if Archi.ptr64 then ".quad" else ".4byte" |