diff options
Diffstat (limited to 'gcc/ada/libgnat/a-strsea.ads')
| -rw-r--r-- | gcc/ada/libgnat/a-strsea.ads | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/gcc/ada/libgnat/a-strsea.ads b/gcc/ada/libgnat/a-strsea.ads index 5651bdc..df1b342 100644 --- a/gcc/ada/libgnat/a-strsea.ads +++ b/gcc/ada/libgnat/a-strsea.ads @@ -50,9 +50,11 @@ pragma Assertion_Policy (Pre => Ignore, with Ada.Strings.Maps; use type Ada.Strings.Maps.Character_Mapping_Function; -package Ada.Strings.Search with SPARK_Mode is +package Ada.Strings.Search with + SPARK_Mode, + Always_Terminates +is pragma Preelaborate; - pragma Annotate (GNATprove, Always_Return, Search); -- The ghost function Match tells whether the slice of Source starting at -- From and of length Pattern'Length matches with Pattern with respect to |