diff options
Diffstat (limited to 'x86/SelectOp.vp')
| -rw-r--r-- | x86/SelectOp.vp | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/x86/SelectOp.vp b/x86/SelectOp.vp index cf0f37ec..378590ce 100644 --- a/x86/SelectOp.vp +++ b/x86/SelectOp.vp @@ -38,7 +38,7 @@ Require Import Coqlib. Require Import Compopts. -Require Import AST Integers Floats. +Require Import AST Integers Floats Builtins. Require Import Op CminorSel. Local Open Scope cminorsel_scope. @@ -568,3 +568,8 @@ Nondetfunction builtin_arg (e: expr) := | Eload chunk (Ainstack ofs) Enil => BA_loadstack chunk ofs | _ => BA e end. + +(** Platform-specific known builtins *) + +Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr := + None. |