[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 f07793f25b100f673a18b0ea6ac8aa0645783144..01693e065dd4c279f284318b5733db723555c7c8 100644 (file)
--- 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 914788cb57f9d019081d140d4b9a7d8827cc3d3e..1ebc428645b1be2cdae717301a991c03cc8dda8d 100644 (file)
--- 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.