diff options
Diffstat (limited to 'arm/SelectOp.vp')
| -rw-r--r-- | arm/SelectOp.vp | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp index 4ea1e1a1..fc2fbe6b 100644 --- a/arm/SelectOp.vp +++ b/arm/SelectOp.vp @@ -199,7 +199,7 @@ Definition mulhu (e1: expr) (e2: expr) := Eop Omulhu (e1 ::: e2 ::: Enil). (** ** Bitwise and, or, xor *) -Nondetfunction andimm (n1: int) (e2: expr) := +Nondetfunction andimm (n1: int) (e2: expr) := if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil else if Int.eq n1 Int.mone then e2 else match e2 with @@ -343,14 +343,14 @@ Nondetfunction compimm (default: comparison -> int -> condition) Eop (Ocmp (negate_condition c)) el else if Int.eq_dec n2 Int.one then Eop (Ocmp c) el - else + else Eop (Ointconst Int.zero) Enil | Cne, Eop (Ocmp c) el => if Int.eq_dec n2 Int.zero then Eop (Ocmp c) el else if Int.eq_dec n2 Int.one then Eop (Ocmp (negate_condition c)) el - else + else Eop (Ointconst Int.one) Enil | _, _ => Eop (Ocmp (default c n2)) (e1 ::: Enil) |