aboutsummaryrefslogtreecommitdiff
path: root/gcc/ada
diff options
context:
space:
mode:
authorYannick Moy <moy@adacore.com>2023-04-20 12:15:16 +0200
committerMarc Poulhiès <poulhies@adacore.com>2023-06-13 09:31:43 +0200
commitf02be8fc6e1d9679d507faa7fd72155addc69ab1 (patch)
treea8fb14e82497a4cfb3cf4ee74b41b97c30b37cb1 /gcc/ada
parentbe3a8f913fbef0231b64143e1eefdc8e45fe391e (diff)
downloadgcc-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.ads2
-rw-r--r--gcc/ada/sem_ch13.adb6
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;