diff options
Diffstat (limited to 'aarch64/Asmblock.v')
| -rw-r--r-- | aarch64/Asmblock.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v index 8f859d55..950e28e9 100644 --- a/aarch64/Asmblock.v +++ b/aarch64/Asmblock.v @@ -1255,7 +1255,7 @@ Definition arith_eval_ppp i v1 v2 := | Pudiv W => Val.maketotal (Val.divu v1 v2) | Pudiv X => Val.maketotal (Val.divlu v1 v2) | Paddext x => Val.addl v1 (eval_extend v2 x) - | Psubext x => Val.subl v2 (eval_extend v2 x) + | Psubext x => Val.subl v1 (eval_extend v2 x) | Pfadd S => Val.addfs v1 v2 | Pfadd D => Val.addf v1 v2 | Pfdiv S => Val.divfs v1 v2 |