@@ -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;
@@ -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;
From: Yannick Moy <moy@adacore.com> 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. Tested on x86_64-pc-linux-gnu, committed on master. --- gcc/ada/libgnat/a-strsup.ads | 2 +- gcc/ada/sem_ch13.adb | 6 +++++- 2 files changed, 6 insertions(+), 2 deletions(-)