diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-15 12:32:09 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-15 12:32:09 +0200 |
| commit | fb9578680d1cd88650e7e6aa9bf1e1ffd8b32f49 (patch) | |
| tree | ad4b3da06dc7621ed64353b52abb92edc8291ff6 /powerpc/TargetPrinter.ml | |
| parent | 9dc0dd73f75875b301c886df40087192d0fad386 (diff) | |
| download | compcert-fb9578680d1cd88650e7e6aa9bf1e1ffd8b32f49.tar.gz compcert-fb9578680d1cd88650e7e6aa9bf1e1ffd8b32f49.zip | |
Removed usage of bne and removed duplicated code for return values of atomics.
Instead of introducing a new bne instruction in Asm.v and the TargetPrinter.ml
I use the equivalent bf instruction. The duplicated code is due to unused return
values of builtins. Now we only emit the additional code for the return value if
the return value is used instead of duplicating the whole emiting sequence.
Diffstat (limited to 'powerpc/TargetPrinter.ml')
| -rw-r--r-- | powerpc/TargetPrinter.ml | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 1f1306c0..eca7a1b8 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -414,13 +414,6 @@ module Target (System : SYSTEM):TARGET = end | Pbl(s, sg) -> fprintf oc " bl %a\n" symbol s - | Pbne lbl -> - fprintf oc " bne- %a\n" label (transl_label lbl) - | Pbne_rel ofs -> - let ofs = camlint_of_coqint ofs in - let sign = if ofs >= 0l then "+" else "-" in - let ofs = Int32.abs ofs in - fprintf oc " bne- $%s%ld\n" sign ofs | Pbs(s, sg) -> fprintf oc " b %a\n" symbol s | Pblr -> |