diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-10-13 16:02:15 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-10-13 16:02:15 +0200 |
| commit | 94becaa726a06ab83a7e5e61f61cab89d5884d62 (patch) | |
| tree | d627edf5c38ae46ff1dc4eccca0199f07caae9c0 /aarch64/Asmblock.v | |
| parent | 10ae0441711eba798e852ca580c5895cb49576d9 (diff) | |
| download | compcert-kvx-94becaa726a06ab83a7e5e61f61cab89d5884d62.tar.gz compcert-kvx-94becaa726a06ab83a7e5e61f61cab89d5884d62.zip | |
Simplifying Ltac and fixing a bug in AsmBlock semantics
The bug was a typo on the PArithPPP subl inst
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 |