diff options
author | Yannick Moy <moy@adacore.com> | 2023-04-20 12:15:16 +0200 |
---|---|---|
committer | Marc Poulhiès <poulhies@adacore.com> | 2023-06-13 09:31:43 +0200 |
commit | f02be8fc6e1d9679d507faa7fd72155addc69ab1 (patch) | |
tree | a8fb14e82497a4cfb3cf4ee74b41b97c30b37cb1 /gcc/ada | |
parent | be3a8f913fbef0231b64143e1eefdc8e45fe391e (diff) | |
download | gcc-f02be8fc6e1d9679d507faa7fd72155addc69ab1.zip gcc-f02be8fc6e1d9679d507faa7fd72155addc69ab1.tar.gz gcc-f02be8fc6e1d9679d507faa7fd72155addc69ab1.tar.bz2 |
ada: Use ghost predicate in standard library
In preparation for attribute Initialized to become ghost, use aspect
Ghost_Predicate instead of Predicate in unit Ada.Strings.Superbounded
of the standard library.
gcc/ada/
* libgnat/a-strsup.ads: Change predicate aspect.
* sem_ch13.adb (Add_Predicate): Fix for first predicate.
Diffstat (limited to 'gcc/ada')
-rw-r--r-- | gcc/ada/libgnat/a-strsup.ads | 2 | ||||
-rw-r--r-- | gcc/ada/sem_ch13.adb | 6 |
2 files changed, 6 insertions, 2 deletions
diff --git a/gcc/ada/libgnat/a-strsup.ads b/gcc/ada/libgnat/a-strsup.ads index 7a8a2ba..2e0cd98 100644 --- a/gcc/ada/libgnat/a-strsup.ads +++ b/gcc/ada/libgnat/a-strsup.ads @@ -69,7 +69,7 @@ package Ada.Strings.Superbounded with SPARK_Mode is -- Leaving it out is more efficient. end record with - Predicate => + Ghost_Predicate => Current_Length <= Max_Length and then Data (1 .. Current_Length)'Initialized, Put_Image => Put_Image; diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb index 32771f0..2b8b64a 100644 --- a/gcc/ada/sem_ch13.adb +++ b/gcc/ada/sem_ch13.adb @@ -10101,9 +10101,13 @@ package body Sem_Ch13 is -- Start of processing for Add_Predicate begin - -- A ghost predicate is checked only when Ghost mode is enabled + -- A ghost predicate is checked only when Ghost mode is enabled. + -- Add a condition for the presence of a predicate to be recorded, + -- which is needed to generate the corresponding predicate + -- function. if Is_Ignored_Ghost_Pragma (Prag) then + Add_Condition (New_Occurrence_Of (Standard_True, Sloc (Prag))); return; end if; |