aboutsummaryrefslogtreecommitdiffstats
path: root/x86/SelectOpproof.v
diff options
context:
space:
mode:
Diffstat (limited to 'x86/SelectOpproof.v')
-rw-r--r--x86/SelectOpproof.v24
1 files changed, 15 insertions, 9 deletions
diff --git a/x86/SelectOpproof.v b/x86/SelectOpproof.v
index b412ccf7..821a54e8 100644
--- a/x86/SelectOpproof.v
+++ b/x86/SelectOpproof.v
@@ -13,15 +13,9 @@
(** Correctness of instruction selection for operators *)
Require Import Coqlib.
-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.
Local Open Scope cminorsel_scope.
@@ -1010,4 +1004,16 @@ Proof.
- constructor; auto.
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.