From fc384f172b72f90c8de52ec846344b7ffda76070 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Mon, 14 Feb 2022 16:19:17 +0100 Subject: compiled absdiff --- kvx/Asmvliw.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kvx/Asmvliw.v') diff --git a/kvx/Asmvliw.v b/kvx/Asmvliw.v index bbd40692..0ce2ed69 100644 --- a/kvx/Asmvliw.v +++ b/kvx/Asmvliw.v @@ -1087,7 +1087,7 @@ Definition arith_eval_rri64 n v i := | Pornil => Val.orl (Val.notl v) (Vlong i) | Paddxil shift => ExtValues.addxl (int_of_shift1_4 shift) v (Vlong i) | Prevsubxil shift => ExtValues.revsubxl (int_of_shift1_4 shift) v (Vlong i) - | Pabdil => ExtValues.absdiff v (Vlong i) + | Pabdil => ExtValues.absdiffl v (Vlong i) end. Definition cmove bt v1 v2 v3 := -- cgit