diff options
| -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; |