diff options
Diffstat (limited to 'mppa_k1c/SelectOp.vp')
| -rw-r--r-- | mppa_k1c/SelectOp.vp | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index 219a462b..ee614253 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -66,7 +66,10 @@ Section SELECT. Context {hf: helper_functions}. (** Ternary operator *) -Definition select (ty : typ) (cond : condition) (args : exprlist) (e1 e2: expr) : option expr := None. +(** TODO *) +Definition select (ty : typ) (cond : condition) (args : exprlist) (e1 e2: expr) : option expr := + Some (Eop (Osel (Ccomp0 Cne) ty) (e1 ::: e2 ::: + (Eop (Ocmp cond) args) ::: Enil)). (** ** Constants **) |