diff options
Diffstat (limited to 'arm/SelectOp.vp')
| -rw-r--r-- | arm/SelectOp.vp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp index 27b5f536..6049017c 100644 --- a/arm/SelectOp.vp +++ b/arm/SelectOp.vp @@ -111,10 +111,10 @@ Nondetfunction addimm (n: int) (e: expr) := Nondetfunction add (e1: expr) (e2: expr) := match e1, e2 with | Eop (Ointconst n1) Enil, t2 => addimm n1 t2 + | t1, Eop (Ointconst n2) Enil => addimm n2 t1 | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) => addimm (Int.add n1 n2) (Eop Oadd (t1:::t2:::Enil)) | Eop(Oaddimm n1) (t1:::Enil), t2 => addimm n1 (Eop Oadd (t1:::t2:::Enil)) - | t1, Eop (Ointconst n2) Enil => addimm n2 t1 | t1, Eop (Oaddimm n2) (t2:::Enil) => addimm n2 (Eop Oadd (t1:::t2:::Enil)) | Eop (Oshift s) (t1:::Enil), t2 => Eop (Oaddshift s) (t2:::t1:::Enil) | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oaddshift s) (t1:::t2:::Enil) |