From 26775b65ba98ad798fc72c92ae73bd28609aaeb8 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Sat, 1 Jun 2019 08:48:20 +0200
Subject: ARM: select is not supported at type Tlong

---
 arm/SelectOp.vp     | 9 ++++++++-
 arm/SelectOpproof.v | 4 +++-
 2 files changed, 11 insertions(+), 2 deletions(-)

(limited to 'arm')

diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp
index 61ea6283..d04832d6 100644
--- a/arm/SelectOp.vp
+++ b/arm/SelectOp.vp
@@ -383,7 +383,14 @@ Definition compfs (c: comparison) (e1: expr) (e2: expr) :=
   Eop (Ocmp (Ccompfs c)) (e1 ::: e2 ::: Enil).
 
 Definition select (ty: typ) (cond: condition) (args: exprlist) (e1 e2: expr) :=
-  Some (Eop (Osel cond ty) (e1 ::: e2 ::: args)).
+  if match ty with
+     | Tint => true
+     | Tfloat => true
+     | Tsingle => true
+     | _ => false
+     end
+  then Some (Eop (Osel cond ty) (e1 ::: e2 ::: args))
+  else None.
 
 (** ** Integer conversions *)
 
diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v
index f281f7ce..8b546971 100644
--- a/arm/SelectOpproof.v
+++ b/arm/SelectOpproof.v
@@ -746,7 +746,9 @@ Theorem eval_select:
      eval_expr ge sp e m le a v
   /\ Val.lessdef (Val.select (Some b) v1 v2 ty) v.
 Proof.
-  unfold select; intros; inv H. rewrite <- H3; TrivialExists. 
+  unfold select; intros.
+  destruct (match ty with Tint | Tfloat | Tsingle => true | _ => false end); inv H.
+  rewrite <- H3; TrivialExists. 
 Qed.
 
 Theorem eval_cast8signed: unary_constructor_sound cast8signed (Val.sign_ext 8).
-- 
cgit