aboutsummaryrefslogtreecommitdiffstats
path: root/riscV/TargetPrinter.ml
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2021-02-02 10:21:17 +0100
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2021-02-02 10:21:17 +0100
commitd2159e300b2d5e017a3144c747d34949b2ff2769 (patch)
tree2186636bc3f2e85b5effd19f9e7c23f4183545aa /riscV/TargetPrinter.ml
parente0f1a90c2dcf7c43137064470ce4b12368b8435d (diff)
downloadcompcert-kvx-d2159e300b2d5e017a3144c747d34949b2ff2769.tar.gz
compcert-kvx-d2159e300b2d5e017a3144c747d34949b2ff2769.zip
begin implementing select
Diffstat (limited to 'riscV/TargetPrinter.ml')
-rw-r--r--riscV/TargetPrinter.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml
index 4bcfa6af..1f00c440 100644
--- a/riscV/TargetPrinter.ml
+++ b/riscV/TargetPrinter.ml
@@ -529,6 +529,8 @@ module Target : TARGET =
fprintf oc " fcvt.s.d %a, %a\n" freg fd freg fs
(* Pseudo-instructions expanded in Asmexpand *)
+ | Pselectl(_, _, _, _) ->
+ assert false
| Pallocframe(sz, ofs) ->
assert false
| Pfreeframe(sz, ofs) ->