aboutsummaryrefslogtreecommitdiffstats
path: root/verilog/PrintOp.ml
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2023-04-27 16:32:13 +0100
committerYann Herklotz <git@yannherklotz.com>2023-04-27 16:32:13 +0100
commitab617cf8e6e60e8de3eb8de220f71dd05c18209f (patch)
tree1e2da8e3edbf48d02f536a21f2cafb6167045c51 /verilog/PrintOp.ml
parentf0867a37e28a1f3670362e7935f9ef30988ddb92 (diff)
downloadcompcert-ab617cf8e6e60e8de3eb8de220f71dd05c18209f.tar.gz
compcert-ab617cf8e6e60e8de3eb8de220f71dd05c18209f.zip
Update verilog back end with new x86 changesHEADmaster
Diffstat (limited to 'verilog/PrintOp.ml')
-rw-r--r--verilog/PrintOp.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/verilog/PrintOp.ml b/verilog/PrintOp.ml
index 6aa4d450..ac2e8f49 100644
--- a/verilog/PrintOp.ml
+++ b/verilog/PrintOp.ml
@@ -147,6 +147,8 @@ let print_operation reg pp = function
| Osubf, [r1;r2] -> fprintf pp "%a -f %a" reg r1 reg r2
| Omulf, [r1;r2] -> fprintf pp "%a *f %a" reg r1 reg r2
| Odivf, [r1;r2] -> fprintf pp "%a /f %a" reg r1 reg r2
+ | Omaxf, [r1;r2] -> fprintf pp "max(%a, %a)" reg r1 reg r2
+ | Ominf, [r1;r2] -> fprintf pp "min(%a, %a)" reg r1 reg r2
| Onegfs, [r1] -> fprintf pp "negfs(%a)" reg r1
| Oabsfs, [r1] -> fprintf pp "absfs(%a)" reg r1
| Oaddfs, [r1;r2] -> fprintf pp "%a +fs %a" reg r1 reg r2