diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-01-24 10:04:21 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-01-24 10:04:21 +0100 |
| commit | db85b47c5487ddfa051b01e444d2be555013e7f7 (patch) | |
| tree | bc571949e44e7fb17da952a4fb5caaf8668976fb /kvx | |
| parent | 3b36bd818ffc20f7a455da46a89641c02491a4e1 (diff) | |
| download | compcert-kvx-db85b47c5487ddfa051b01e444d2be555013e7f7.tar.gz compcert-kvx-db85b47c5487ddfa051b01e444d2be555013e7f7.zip | |
progress
Diffstat (limited to 'kvx')
| -rw-r--r-- | kvx/FPDivision64.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index 6894460f..9ed12064 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -1108,7 +1108,7 @@ Qed. Definition step2_real_div_long a b := Val.mulf (Val.maketotal (Val.floatoflong a)) (approx_inv_longu b). -Definition smalla_thresh := 35184372088832%Z. +Definition smalla_thresh := 34184372088832%Z. Lemma step2_real_div_long_smalla_correct : forall (a b : int64) @@ -1116,7 +1116,7 @@ Lemma step2_real_div_long_smalla_correct : (b_NOT0 : (0 < Int64.unsigned b)%Z), exists (q : float), (step2_real_div_long (Vlong a) (Vlong b)) = Vfloat q /\ - (Rabs ((B2R _ _ q) - (IZR (Int64.signed a)) / (IZR (Int64.unsigned b))) <= (255/256))%R. + (Rabs ((B2R _ _ q) - (IZR (Int64.signed a)) / (IZR (Int64.unsigned b))) <= (32767/65536))%R. Proof. intros. unfold step2_real_div_long. |