From: Yannick Moy Date: Fri, 17 Dec 2021 16:45:14 +0000 (+0100) Subject: [Ada] Proof of unit System.Case_Util X-Git-Tag: basepoints/gcc-13~1859 X-Git-Url: http://git.ipfire.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=303bd2a8428b75f2467578a933e729d5672789d1;p=thirdparty%2Fgcc.git [Ada] Proof of unit System.Case_Util gcc/ada/ * libgnat/s-casuti.adb: Add ghost code. * libgnat/s-casuti.ads: Add contracts. --- diff --git a/gcc/ada/libgnat/s-casuti.adb b/gcc/ada/libgnat/s-casuti.adb index f07793f25b10..01693e065dd4 100644 --- a/gcc/ada/libgnat/s-casuti.adb +++ b/gcc/ada/libgnat/s-casuti.adb @@ -29,8 +29,17 @@ -- -- ------------------------------------------------------------------------------ -package body System.Case_Util is +-- Ghost code, loop invariants and assertions in this unit are meant for +-- analysis only, not for run-time checking, as it would be too costly +-- otherwise. This is enforced by setting the assertion policy to Ignore. +pragma Assertion_Policy (Ghost => Ignore, + Loop_Invariant => Ignore, + Assert => Ignore); + +package body System.Case_Util + with SPARK_Mode +is -------------- -- To_Lower -- -------------- @@ -53,6 +62,9 @@ package body System.Case_Util is begin for J in A'Range loop A (J) := To_Lower (A (J)); + + pragma Loop_Invariant + (for all K in A'First .. J => A (K) = To_Lower (A'Loop_Entry (K))); end loop; end To_Lower; @@ -78,6 +90,15 @@ package body System.Case_Util is A (J) := To_Lower (A (J)); end if; + pragma Loop_Invariant + (for all K in A'First .. J => + (if K = A'First + or else A'Loop_Entry (K - 1) = '_' + then + A (K) = To_Upper (A'Loop_Entry (K)) + else + A (K) = To_Lower (A'Loop_Entry (K)))); + Ucase := A (J) = '_'; end loop; end To_Mixed; @@ -111,6 +132,9 @@ package body System.Case_Util is begin for J in A'Range loop A (J) := To_Upper (A (J)); + + pragma Loop_Invariant + (for all K in A'First .. J => A (K) = To_Upper (A'Loop_Entry (K))); end loop; end To_Upper; diff --git a/gcc/ada/libgnat/s-casuti.ads b/gcc/ada/libgnat/s-casuti.ads index 914788cb57f9..1ebc428645b1 100644 --- a/gcc/ada/libgnat/s-casuti.ads +++ b/gcc/ada/libgnat/s-casuti.ads @@ -34,29 +34,98 @@ -- This package provides simple casing functions that do not require the -- overhead of the full casing tables found in Ada.Characters.Handling. -package System.Case_Util is - pragma Pure; +-- Preconditions in this unit are meant for analysis only, not for run-time +-- checking, so that the expected exceptions are raised. This is enforced by +-- setting the corresponding assertion policy to Ignore. Postconditions and +-- contract cases should not be executed at runtime as well, in order not to +-- slow down the execution of these functions. +pragma Assertion_Policy (Pre => Ignore, + Post => Ignore, + Contract_Cases => Ignore, + Ghost => Ignore); + +package System.Case_Util + with Pure, SPARK_Mode +is -- Note: all the following functions handle the full Latin-1 set - function To_Upper (A : Character) return Character; + function To_Upper (A : Character) return Character + with + Post => (declare + A_Val : constant Natural := Character'Pos (A); + begin + (if A in 'a' .. 'z' + or else A_Val in 16#E0# .. 16#F6# + or else A_Val in 16#F8# .. 16#FE# + then + To_Upper'Result = Character'Val (A_Val - 16#20#) + else + To_Upper'Result = A)); -- Converts A to upper case if it is a lower case letter, otherwise -- returns the input argument unchanged. - procedure To_Upper (A : in out String); - function To_Upper (A : String) return String; + procedure To_Upper (A : in out String) + with + Post => (for all J in A'Range => A (J) = To_Upper (A'Old (J))); + + function To_Upper (A : String) return String + with + Post => To_Upper'Result'First = A'First + and then To_Upper'Result'Last = A'Last + and then (for all J in A'Range => + To_Upper'Result (J) = To_Upper (A (J))); -- Folds all characters of string A to upper case - function To_Lower (A : Character) return Character; + function To_Lower (A : Character) return Character + with + Post => (declare + A_Val : constant Natural := Character'Pos (A); + begin + (if A in 'A' .. 'Z' + or else A_Val in 16#C0# .. 16#D6# + or else A_Val in 16#D8# .. 16#DE# + then + To_Lower'Result = Character'Val (A_Val + 16#20#) + else + To_Lower'Result = A)); -- Converts A to lower case if it is an upper case letter, otherwise -- returns the input argument unchanged. - procedure To_Lower (A : in out String); - function To_Lower (A : String) return String; + procedure To_Lower (A : in out String) + with + Post => (for all J in A'Range => A (J) = To_Lower (A'Old (J))); + + function To_Lower (A : String) return String + with + Post => To_Lower'Result'First = A'First + and then To_Lower'Result'Last = A'Last + and then (for all J in A'Range => + To_Lower'Result (J) = To_Lower (A (J))); -- Folds all characters of string A to lower case - procedure To_Mixed (A : in out String); - function To_Mixed (A : String) return String; + procedure To_Mixed (A : in out String) + with + Post => + (for all J in A'Range => + (if J = A'First + or else A'Old (J - 1) = '_' + then + A (J) = To_Upper (A'Old (J)) + else + A (J) = To_Lower (A'Old (J)))); + + function To_Mixed (A : String) return String + with + Post => To_Mixed'Result'First = A'First + and then To_Mixed'Result'Last = A'Last + and then (for all J in A'Range => + (if J = A'First + or else A (J - 1) = '_' + then + To_Mixed'Result (J) = To_Upper (A (J)) + else + To_Mixed'Result (J) = To_Lower (A (J)))); -- Converts A to mixed case (i.e. lower case, except for initial -- character and any character after an underscore, which are -- converted to upper case.