diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-06-03 22:26:06 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-06-03 22:26:06 +0200 |
| commit | 487fc42595bb43450f2b0b5a49b4edbc22892b9f (patch) | |
| tree | eb671c210dd1e09651003c4f0add4cca118519a2 /mppa_k1c/SelectLong.vp | |
| parent | 677771949bd62f7f5bbcf99bba6b6f816f07a6c2 (diff) | |
| download | compcert-kvx-487fc42595bb43450f2b0b5a49b4edbc22892b9f.tar.gz compcert-kvx-487fc42595bb43450f2b0b5a49b4edbc22892b9f.zip | |
rm old select/selectl/selectf/selectfs
Diffstat (limited to 'mppa_k1c/SelectLong.vp')
| -rw-r--r-- | mppa_k1c/SelectLong.vp | 19 |
1 files changed, 0 insertions, 19 deletions
diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp index 4e369e11..981c796c 100644 --- a/mppa_k1c/SelectLong.vp +++ b/mppa_k1c/SelectLong.vp @@ -306,14 +306,6 @@ Nondetfunction andl (e1: expr) (e2: expr) := | t1, (Eop Onotl (t2:::Enil)) => Eop Oandnl (t2:::t1:::Enil) | _, _ => Eop Oandl (e1:::e2:::Enil) end. -(* - | (Eop Ocast32signed - ((Eop Oneg ((Eop (Ocmp (Ccomplimm Cne zero1)) - (y1:::Enil)):::Enil)):::Enil)), v1 => - if Int64.eq zero1 Int64.zero - then Eop Oselectl ((Eop (Olongconst Int64.zero) Enil):::v1:::y1:::Enil) - else Eop Oandl (e1:::e2:::Enil) -*) Nondetfunction orlimm (n1: int64) (e2: expr) := if Int64.eq n1 Int64.zero then e2 else @@ -332,17 +324,6 @@ Nondetfunction orl (e1: expr) (e2: expr) := | t1, Eop (Olongconst n2) Enil => orlimm n2 t1 | (Eop Onotl (t1:::Enil)), t2 => Eop Oornl (t1:::t2:::Enil) | t1, (Eop Onotl (t2:::Enil)) => Eop Oornl (t2:::t1:::Enil) - | (Eop Oandl ((Eop Ocast32signed - ((Eop Oneg ((Eop (Ocmp (Ccomplimm Ceq zero0)) - (y0:::Enil)):::Enil)):::Enil)):::v0:::Enil)), - (Eop Oandl ((Eop Ocast32signed - ((Eop Oneg ((Eop (Ocmp (Ccomplimm Cne zero1)) - (y1:::Enil)):::Enil)):::Enil)):::v1:::Enil)) => - if same_expr_pure y0 y1 - && Int64.eq zero0 Int64.zero - && Int64.eq zero1 Int64.zero - then Eop (Oselectl (Ccompl0 Cne)) (v0:::v1:::y0:::Enil) - else Eop Oorl (e1:::e2:::Enil) | (Eop (Oandlimm nmask) (prev:::Enil)), (Eop (Oandlimm mask) ((Eop (Oshllimm start) (fld:::Enil)):::Enil)) => |