diff options
Diffstat (limited to 'cfrontend/Csyntax.v')
-rw-r--r-- | cfrontend/Csyntax.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v index 00565309..c34a5e13 100644 --- a/cfrontend/Csyntax.v +++ b/cfrontend/Csyntax.v @@ -100,6 +100,18 @@ Definition Epreincr (id: incr_or_decr) (l: expr) (ty: type) := Eassignop (match id with Incr => Oadd | Decr => Osub end) l (Eval (Vint Int.one) type_int32s) (typeconv ty) ty. +(** Selection is a conditional expression that always evaluates both arms + and can be implemented by "conditional move" instructions. + It is expressed as an invocation of a builtin function. *) + +Definition Eselection (r1 r2 r3: expr) (ty: type) := + let t := typ_of_type ty in + let sg := mksignature (AST.Tint :: t :: t :: nil) (Some t) cc_default in + Ebuiltin (EF_builtin "__builtin_sel"%string sg) + (Tcons type_bool (Tcons ty (Tcons ty Tnil))) + (Econs r1 (Econs r2 (Econs r3 Enil))) + ty. + (** Extract the type part of a type-annotated expression. *) Definition typeof (a: expr) : type := |