From 24406a351e9d64c2953b0b9fc7ef0b3d79db9b85 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Fri, 20 Sep 2019 18:51:54 +0200
Subject: fix compiling for aarch64

---
 aarch64/SelectOp.vp | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'aarch64/SelectOp.vp')

diff --git a/aarch64/SelectOp.vp b/aarch64/SelectOp.vp
index 5bd96987..f9e5a1c4 100644
--- a/aarch64/SelectOp.vp
+++ b/aarch64/SelectOp.vp
@@ -547,6 +547,13 @@ Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=
   | _ => (Aindexed Int64.zero, e:::Enil)
   end.
 
+(* floats *)
+Definition divf_base (e1: expr) (e2: expr) :=
+  Eop Odivf (e1 ::: e2 ::: Enil).
+
+Definition divfs_base (e1: expr) (e2: expr) :=
+  Eop Odivfs (e1 ::: e2 ::: Enil).
+
 (** ** Arguments of builtins *)
 
 Nondetfunction builtin_arg (e: expr) :=
-- 
cgit