diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-20 13:32:18 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-20 13:32:18 +0200 |
| commit | 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f (patch) | |
| tree | 1961b41815fc6e392cc0bd2beeb0fb504bc160ce /arm/Asmgen.v | |
| parent | 7a6bb90048db7a254e959b1e3c308bac5fe6c418 (diff) | |
| download | compcert-kvx-4d542bc7eafadb16b845cf05d1eb4988eb55ed0f.tar.gz compcert-kvx-4d542bc7eafadb16b845cf05d1eb4988eb55ed0f.zip | |
Updated PR by removing whitespaces. Bug 17450.
Diffstat (limited to 'arm/Asmgen.v')
| -rw-r--r-- | arm/Asmgen.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/arm/Asmgen.v b/arm/Asmgen.v index 2365d1d2..7b3f2fdc 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -198,7 +198,7 @@ Definition rsubimm (r1 r2: ireg) (n: int) (k: code) := iterate_op (Prsb r1 r2) (Padd r1 r1) (decompose_int n) k. Definition andimm (r1 r2: ireg) (n: int) (k: code) := - if is_immed_arith n + if is_immed_arith n then Pand r1 r2 (SOimm n) :: k else iterate_op (Pbic r1 r2) (Pbic r1 r1) (decompose_int (Int.not n)) k. @@ -402,7 +402,7 @@ Definition transl_op do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (Pmul r r1 r2 :: k) | Omla, a1 :: a2 :: a3 :: nil => - do r <- ireg_of res; do r1 <- ireg_of a1; + do r <- ireg_of res; do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r3 <- ireg_of a3; OK (Pmla r r1 r2 r3 :: k) | Omulhs, a1 :: a2 :: nil => |