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.
-- 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;
-- 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;