From c1e007985fef1389ba09f5b558aa4e7b9f03783f Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Fri, 11 Mar 2022 11:54:53 +0100 Subject: [PATCH] [Ada] Fix proof of double arithmetic units Proof of an assertion is not automatic anymore. Add two assertions before it to guide the prover. gcc/ada/ * libgnat/s-aridou.adb (Double_Divide): Add intermediate assertions. --- gcc/ada/libgnat/s-aridou.adb | 2 ++ 1 file changed, 2 insertions(+) diff --git a/gcc/ada/libgnat/s-aridou.adb b/gcc/ada/libgnat/s-aridou.adb index ffb6f4ca269..08cbed7cefc 100644 --- a/gcc/ada/libgnat/s-aridou.adb +++ b/gcc/ada/libgnat/s-aridou.adb @@ -941,11 +941,13 @@ is else T2 := Yhi * Zlo; pragma Assert (Big (T2) = Big (Double_Uns'(Yhi * Zlo))); + pragma Assert (Big_0 = Big (Double_Uns'(Ylo * Zhi))); end if; else T2 := Ylo * Zhi; pragma Assert (Big (T2) = Big (Double_Uns'(Ylo * Zhi))); + pragma Assert (Big_0 = Big (Double_Uns'(Yhi * Zlo))); end if; T1 := Ylo * Zlo; -- 2.47.2