1 files changed, 16 insertions, 11 deletions
diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v
index f7dd8dd6..75d32ea3 100644
--- a/arm/SelectOpproof.v
+++ b/arm/SelectOpproof.v
@@ -13,16 +13,9 @@
 (** Correctness of instruction selection for operators *)
 
 Require Import Coqlib.
-Require Import Maps.
-Require Import AST.
-Require Import Integers.
-Require Import Floats.
-Require Import Values.
-Require Import Memory.
-Require Import Globalenvs.
-Require Import Cminor.
-Require Import Op.
-Require Import CminorSel.
+Require Import AST Integers Floats.
+Require Import Values Memory Builtins Globalenvs.
+Require Import Cminor Op CminorSel.
 Require Import SelectOp.
 Require Import OpHelpers OpHelpersproof.
 
@@ -912,7 +905,6 @@ Proof.
 - constructor; auto.
 Qed.
 
-
 (* floating-point division without HELPERS *)
 Theorem eval_divf_base:
   forall le a b x y,
@@ -933,4 +925,17 @@ Proof.
   intros; unfold divfs_base.
   TrivialExists.
 Qed.
+
+(** Platform-specific known builtins *)
+
+Theorem eval_platform_builtin:
+  forall bf al a vl v le,
+  platform_builtin bf al = Some a ->
+  eval_exprlist ge sp e m le al vl ->
+  platform_builtin_sem bf vl = Some v ->
+  exists v', eval_expr ge sp e m le a v' /\ Val.lessdef v v'.
+Proof.
+  intros. discriminate.
+Qed.
+
 End CMCONSTR.