diff options
| author | Michael Schmidt <github@mschmidt.me> | 2015-10-14 15:26:56 +0200 |
|---|---|---|
| committer | Michael Schmidt <github@mschmidt.me> | 2015-10-14 15:26:56 +0200 |
| commit | f5bb397acd12292f6b41438778f2df7391d6f2fe (patch) | |
| tree | b5964ca4c395b0db639565d0d0fddc9c44e34cf1 /arm/Asmgen.v | |
| parent | fd83d08d27057754202c575ed8a42d01b1af54c5 (diff) | |
| download | compcert-f5bb397acd12292f6b41438778f2df7391d6f2fe.tar.gz compcert-f5bb397acd12292f6b41438778f2df7391d6f2fe.zip | |
bug 17392: remove trailing whitespace in source files
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 => |