aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc/TargetPrinter.ml
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-12-08 09:17:41 +0100
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-12-08 09:17:41 +0100
commitcb93a301fd2ddae3071ae0838290b201496d90ef (patch)
treeb1531d98e7c7e57a2c56e0550cb0e354278f1016 /powerpc/TargetPrinter.ml
parent23da7b35d0edf98f271401ac93a1fa06adb062a2 (diff)
parentb40aef6c55b837786cd749260e8e8d8a1d328034 (diff)
downloadcompcert-kvx-cb93a301fd2ddae3071ae0838290b201496d90ef.tar.gz
compcert-kvx-cb93a301fd2ddae3071ae0838290b201496d90ef.zip
Merge github.com:AbsInt/CompCert into kvx-workv3.8_kvx_instructions_fixed
Diffstat (limited to 'powerpc/TargetPrinter.ml')
-rw-r--r--powerpc/TargetPrinter.ml6
1 files changed, 0 insertions, 6 deletions
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index 3ea03786..554bfe09 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -557,22 +557,16 @@ module Target (System : SYSTEM):TARGET =
fprintf oc " fadds %a, %a, %a\n" freg r1 freg r2 freg r3
| Pfcmpu(r1, r2) ->
fprintf oc " fcmpu %a, %a, %a\n" creg 0 freg r1 freg r2
- | Pfcfi(r1, r2) ->
- assert false
| Pfcfl(r1, r2) ->
assert false
| Pfcfid(r1, r2) ->
fprintf oc " fcfid %a, %a\n" freg r1 freg r2
- | Pfcfiu(r1, r2) ->
- assert false
| Pfcti(r1, r2) ->
assert false
| Pfctid(r1, r2) ->
assert false
| Pfctidz(r1, r2) ->
fprintf oc " fctidz %a, %a\n" freg r1 freg r2
- | Pfctiu(r1, r2) ->
- assert false
| Pfctiw(r1, r2) ->
fprintf oc " fctiw %a, %a\n" freg r1 freg r2
| Pfctiwz(r1, r2) ->