From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: by sourceware.org (Postfix, from userid 7871) id 510EC3858D3C; Tue, 20 Jun 2023 07:46:11 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 510EC3858D3C DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1687247171; bh=qrEApRm5qOMchWU94InjEDTlbSDlXaiPuGinsMQxVpU=; h=From:To:Subject:Date:From; b=kAZgxHuufZaJcSAdgGDKeFgrP7km2toPnHN4pO49TKyU45Xdof5uAO8IQqIfGaWFm jY6rk9QtGxkJ6uOaC9uF0ejVLHoSi1pkMlaOAUL5XBUFQTuCYEJZvqgV4WFCxEgdNn 8JkQeZuhWKmXtBksT+GD0S3x9+jbIjuqz8mKe/sU= MIME-Version: 1.0 Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset="utf-8" From: Marc Poulhi?s To: gcc-cvs@gcc.gnu.org Subject: [gcc r14-1965] ada: Update annotations in runtime for proof X-Act-Checkin: gcc X-Git-Author: Yannick Moy X-Git-Refname: refs/heads/master X-Git-Oldrev: ca27b8a030746d09ea61de62e1f3bc1337ebe737 X-Git-Newrev: adc853f0661dcb4d1204d1a89ed49446ec01a980 Message-Id: <20230620074611.510EC3858D3C@sourceware.org> Date: Tue, 20 Jun 2023 07:46:11 +0000 (GMT) List-Id: https://gcc.gnu.org/g:adc853f0661dcb4d1204d1a89ed49446ec01a980 commit r14-1965-gadc853f0661dcb4d1204d1a89ed49446ec01a980 Author: Yannick Moy Date: Tue May 16 13:16:13 2023 +0000 ada: Update annotations in runtime for proof With bump of stable SPARK used for proof of the runtime, some annotations need to change. gcc/ada/ * libgnat/s-aridou.adb (Scaled_Divide): Add assertions. * libgnat/s-valuti.adb: Add Loop_Variant. * libgnat/s-valuti.ads: Add Exceptional_Cases on No_Return procedure. Diff: --- gcc/ada/libgnat/s-aridou.adb | 11 +++++++++++ gcc/ada/libgnat/s-valuti.adb | 2 ++ gcc/ada/libgnat/s-valuti.ads | 3 ++- 3 files changed, 15 insertions(+), 1 deletion(-) diff --git a/gcc/ada/libgnat/s-aridou.adb b/gcc/ada/libgnat/s-aridou.adb index 66ace8071ff..831590ce387 100644 --- a/gcc/ada/libgnat/s-aridou.adb +++ b/gcc/ada/libgnat/s-aridou.adb @@ -2580,8 +2580,19 @@ is pragma Assert (Big (Double_Uns (Hi (T2))) + Big (Double_Uns (Hi (T1))) = Big (Double_Uns (D (1)))); + pragma Assert + (Is_Mult_Decomposition (D1 => Big (Double_Uns (D (1))), + D2 => Big (Double_Uns (D (2))), + D3 => Big (Double_Uns (D (3))), + D4 => Big (Double_Uns (D (4))))); else D (1) := 0; + + pragma Assert + (Is_Mult_Decomposition (D1 => Big (Double_Uns (D (1))), + D2 => Big (Double_Uns (D (2))), + D3 => Big (Double_Uns (D (3))), + D4 => Big (Double_Uns (D (4))))); end if; else diff --git a/gcc/ada/libgnat/s-valuti.adb b/gcc/ada/libgnat/s-valuti.adb index ec6fdb03225..ee37c1a636b 100644 --- a/gcc/ada/libgnat/s-valuti.adb +++ b/gcc/ada/libgnat/s-valuti.adb @@ -123,6 +123,7 @@ is while F < L and then S (F) = ' ' loop pragma Loop_Invariant (F in S'First .. L - 1); pragma Loop_Invariant (for all J in S'First .. F => S (J) = ' '); + pragma Loop_Variant (Increases => F); F := F + 1; end loop; @@ -139,6 +140,7 @@ is while S (L) = ' ' loop pragma Loop_Invariant (L in F + 1 .. S'Last); pragma Loop_Invariant (for all J in L .. S'Last => S (J) = ' '); + pragma Loop_Variant (Decreases => L); L := L - 1; end loop; diff --git a/gcc/ada/libgnat/s-valuti.ads b/gcc/ada/libgnat/s-valuti.ads index 1faa6471d0d..22d0612bc32 100644 --- a/gcc/ada/libgnat/s-valuti.ads +++ b/gcc/ada/libgnat/s-valuti.ads @@ -51,7 +51,8 @@ is procedure Bad_Value (S : String) with - Depends => (null => S); + Depends => (null => S), + Exceptional_Cases => (others => Standard.False); pragma No_Return (Bad_Value); -- Raises constraint error with message: bad input for 'Value: "xxx"