From f02be8fc6e1d9679d507faa7fd72155addc69ab1 Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Thu, 20 Apr 2023 12:15:16 +0200 Subject: [PATCH] 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. --- gcc/ada/libgnat/a-strsup.ads | 2 +- 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 7a8a2bac996..2e0cd98f8d4 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 32771f06d76..2b8b64aa392 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; -- 2.11.4.GIT