This unit is needed to prove System.Val_Bool, as it is used in
System.Val_Util called from System.Val_Bool. Add contracts that reflect
the implementation, as we don't want these units to depend on units
under Ada.Characters.
Tested on x86_64-pc-linux-gnu, committed on trunk
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
--- 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
--- 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.
