diff options
Diffstat (limited to 'kvx/FPDivision64.v')
-rw-r--r-- | kvx/FPDivision64.v | 13 |
1 files changed, 13 insertions, 0 deletions
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. + + |