diff options
Diffstat (limited to 'mppa_k1c/SelectLong.vp')
| -rw-r--r-- | mppa_k1c/SelectLong.vp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp index 7fefe594..f8f5bf3b 100644 --- a/mppa_k1c/SelectLong.vp +++ b/mppa_k1c/SelectLong.vp @@ -286,6 +286,7 @@ 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 Oorl (e1:::e2:::Enil) end. (* @@ -300,7 +301,6 @@ Nondetfunction orl (e1: expr) (e2: expr) := && Int64.eq zero1 Int64.zero then Eop Oselectl (v0:::v1:::y0:::Enil) else Eop Oorl (e1:::e2:::Enil) - | _, _ => Eop Oorl (e1:::e2:::Enil) *) Nondetfunction xorlimm (n1: int64) (e2: expr) := |