From 82d72ac1253b2c45dbc8f305349611ea2eae0675 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 25 Jan 2022 12:19:05 +0100 Subject: attempt at definition --- kvx/FPDivision64.v | 13 +++++++++++++ 1 file changed, 13 insertions(+) (limited to 'kvx') diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index e57f0d66..1739e5cf 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -1948,3 +1948,16 @@ Proof. } reflexivity. Qed. + +Definition full_div_longu a b m := + let is_big := Val.cmpl_bool Clt b (Vlong Int64.zero) in + let is_one := Val.cmplu_bool (Mem.valid_pointer m) Cle b (Vlong Int64.one) in + let is_special := Val.or (Val.of_optbool is_big) (Val.of_optbool is_one) in + let if_big := Val.select (Val.cmplu_bool (Mem.valid_pointer m) Clt a b) + (Vlong Int64.zero) (Vlong Int64.one) Tlong in + let if_special := Val.select is_big if_big a Tlong in + Val.select (Val.cmp_bool Cne is_special (Vlong Int64.zero)) + if_special + (anystep_div_longu a b m) Tlong. + + -- cgit