diff options
Diffstat (limited to 'mppa_k1c/SelectOp.vp')
| -rw-r--r-- | mppa_k1c/SelectOp.vp | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index 01985060..2618983b 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -91,8 +91,14 @@ Nondetfunction cond_to_condition0 (cond : condition) (args : exprlist) := end. (** Ternary operator *) -Definition select0 (ty : typ) (cond0 : condition0) (e1 e2 eC: expr) := - (Eop (Osel cond0 ty) (e1 ::: e2 ::: eC ::: Enil)). +Nondetfunction select0 (ty : typ) (cond0 : condition0) (e1 e2 e3: expr) := + match ty, cond0, e1, e2, e3 with + | Tint, cond0, e1, (Eop (Ointconst imm) Enil), e3 => + (Eop (Oselimm cond0 imm) (e1 ::: e3 ::: Enil)) + | Tlong, cond0, e1, (Eop (Olongconst imm) Enil), e3 => + (Eop (Osellimm cond0 imm) (e1 ::: e3 ::: Enil)) + | _, _, _ => (Eop (Osel cond0 ty) (e1 ::: e2 ::: e3 ::: Enil)) + end. Definition select (ty : typ) (cond : condition) (args : exprlist) (e1 e2: expr) : option expr := Some( |