From 94becaa726a06ab83a7e5e61f61cab89d5884d62 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 13 Oct 2020 16:02:15 +0200 Subject: Simplifying Ltac and fixing a bug in AsmBlock semantics The bug was a typo on the PArithPPP subl inst --- aarch64/Asmblock.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'aarch64/Asmblock.v') 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 -- cgit