[Ada] Proof of Boolean'Image and Boolean'Value

gcc/ada/

	* libgnat/s-imgboo.adb: Mark in SPARK.
	* libgnat/s-imgboo.ads: Mark in SPARK. Change from Pure to
	Preelaborate unit in order to be able to depend on
	System.Val_Bool.
	(Image_Boolean): Functionally specify the result of the
	procedure by calling System.Val_Bool.Value_Boolean on the
	result.
	* libgnat/s-valboo.adb: Mark in SPARK.
	(First_Non_Space_Ghost): New ghost function.
	(Value_Boolean): Change type of L and F to avoid possible range
	check failure on empty Str.
	* libgnat/s-valboo.ads: Mark in SPARK. Duplicate with-clause
	from body in the spec to be able to call
	System.Val_Util.Only_Space_Ghost in the contract.
	(First_Non_Space_Ghost): New ghost function computing the first
	non-space character in a string.
	(Is_Boolean_Image_Ghost): New ghost function computing whether a
	string is the image of a boolean value.
	(Value_Boolean): Add in precondition the conditions to avoid
	raising Constraint_Error. This precondition is never executed,
	and only used in proof, thanks to the use of pragma
	Assertion_Policy. Given that precondition, the postcondition can
	simply check the first non-space character to decide whether
	True or False is read.
	* libgnat/s-valuti.adb: Mark in SPARK, but use SPARK_Mode Off on
	all subprograms not yet proved.
	(Bad_Value): Annotate expected exception.
	(Normalize_String): Rewrite to avoid possible overflow when
	incrementing F in the first loop. Add loop invariants.
	* libgnat/s-valuti.ads: Mark in SPARK.
	(Bad_Value): Add Depends contract to avoid warning on unused S.
	(Only_Space_Ghost): New ghost function to query if string has
	only space in the specified range.
	(Normalize_String): Add functional contract.
	(Scan_Exponent): Mark spec as not in SPARK as this function has
	side-effects.

6 files changed, 217 insertions, 19 deletions

diff --git a/gcc/ada/libgnat/s-imgboo.adb b/gcc/ada/libgnat/s-imgboo.adb
index 69ee639..4c1f7c9 100644
--- a/gcc/ada/libgnat/s-imgboo.adb
+++ b/gcc/ada/libgnat/s-imgboo.adb
@@ -29,7 +29,17 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
-package body System.Img_Bool 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.Img_Bool
+  with SPARK_Mode
+is
 
    -------------------
    -- Image_Boolean --
diff --git a/gcc/ada/libgnat/s-imgboo.ads b/gcc/ada/libgnat/s-imgboo.ads
index 45b3bfa..35de7ef 100644
--- a/gcc/ada/libgnat/s-imgboo.ads
+++ b/gcc/ada/libgnat/s-imgboo.ads
@@ -31,13 +31,33 @@
 
 --  Boolean'Image
 
-package System.Img_Bool 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);
+
+with System.Val_Bool;
+
+package System.Img_Bool
+  with SPARK_Mode, Preelaborate
+is
 
    procedure Image_Boolean
      (V : Boolean;
       S : in out String;
-      P : out Natural);
+      P : out Natural)
+   with
+     Pre  => S'First = 1
+       and then (if V then S'Length >= 4 else S'Length >= 5),
+     Post => (if V then P = 4 else P = 5)
+       and then System.Val_Bool.Is_Boolean_Image_Ghost (S (1 .. P))
+       and then System.Val_Bool.Value_Boolean (S (1 .. P)) = V;
    --  Computes Boolean'Image (V) and stores the result in S (1 .. P)
    --  setting the resulting value of P. The caller guarantees that S
    --  is long enough to hold the result, and that S'First is 1.
diff --git a/gcc/ada/libgnat/s-valboo.adb b/gcc/ada/libgnat/s-valboo.adb
index 4ec1e19..edfa09a 100644
--- a/gcc/ada/libgnat/s-valboo.adb
+++ b/gcc/ada/libgnat/s-valboo.adb
@@ -29,22 +29,47 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
+--  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);
+
 with System.Val_Util; use System.Val_Util;
 
-package body System.Val_Bool is
+package body System.Val_Bool
+  with SPARK_Mode
+is
+
+   function First_Non_Space_Ghost (S : String) return Positive is
+   begin
+      for J in S'Range loop
+         if S (J) /= ' ' then
+            return J;
+         end if;
+
+         pragma Loop_Invariant (for all K in S'First .. J => S (K) = ' ');
+      end loop;
+
+      raise Program_Error;
+   end First_Non_Space_Ghost;
 
    -------------------
    -- Value_Boolean --
    -------------------
 
    function Value_Boolean (Str : String) return Boolean is
-      F : Natural;
-      L : Natural;
+      F : Integer;
+      L : Integer;
       S : String (Str'Range) := Str;
 
    begin
       Normalize_String (S, F, L);
 
+      pragma Assert (F = First_Non_Space_Ghost (S));
+
       if S (F .. L) = "TRUE" then
          return True;
 
diff --git a/gcc/ada/libgnat/s-valboo.ads b/gcc/ada/libgnat/s-valboo.ads
index 2129c5ac..d8bed1a 100644
--- a/gcc/ada/libgnat/s-valboo.ads
+++ b/gcc/ada/libgnat/s-valboo.ads
@@ -29,10 +29,70 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
-package System.Val_Bool is
+--  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);
+
+with System.Val_Util;
+
+package System.Val_Bool
+  with SPARK_Mode
+is
    pragma Preelaborate;
 
-   function Value_Boolean (Str : String) return Boolean;
+   function First_Non_Space_Ghost (S : String) return Positive
+   with
+     Ghost,
+     Pre  => not System.Val_Util.Only_Space_Ghost (S, S'First, S'Last),
+     Post => First_Non_Space_Ghost'Result in S'Range
+       and then S (First_Non_Space_Ghost'Result) /= ' '
+       and then System.Val_Util.Only_Space_Ghost
+         (S, S'First, First_Non_Space_Ghost'Result - 1);
+   --  Ghost function that returns the index of the first non-space character
+   --  in S, which necessarily exists given the precondition on S.
+
+   function Is_Boolean_Image_Ghost (Str : String) return Boolean is
+     (not System.Val_Util.Only_Space_Ghost (Str, Str'First, Str'Last)
+        and then
+      (declare
+         F : constant Positive := First_Non_Space_Ghost (Str);
+       begin
+         (F <= Str'Last - 3
+          and then Str (F)     in 't' | 'T'
+          and then Str (F + 1) in 'r' | 'R'
+          and then Str (F + 2) in 'u' | 'U'
+          and then Str (F + 3) in 'e' | 'E'
+          and then
+            (if F + 3 < Str'Last then
+               System.Val_Util.Only_Space_Ghost (Str, F + 4, Str'Last)))
+           or else
+         (F <= Str'Last - 4
+          and then Str (F)     in 'f' | 'F'
+          and then Str (F + 1) in 'a' | 'A'
+          and then Str (F + 2) in 'l' | 'L'
+          and then Str (F + 3) in 's' | 'S'
+          and then Str (F + 4) in 'e' | 'E'
+          and then
+            (if F + 4 < Str'Last then
+               System.Val_Util.Only_Space_Ghost (Str, F + 5, Str'Last)))))
+   with
+     Ghost;
+   --  Ghost function that returns True iff Str is the image of a boolean, that
+   --  is "true" or "false" in any capitalization, possibly surounded by space
+   --  characters.
+
+   function Value_Boolean (Str : String) return Boolean
+   with
+     Pre  => Is_Boolean_Image_Ghost (Str),
+     Post =>
+       Value_Boolean'Result = (Str (First_Non_Space_Ghost (Str)) in 't' | 'T');
    --  Computes Boolean'Value (Str)
 
 end System.Val_Bool;
diff --git a/gcc/ada/libgnat/s-valuti.adb b/gcc/ada/libgnat/s-valuti.adb
index 31edc40..e2ae9e3 100644
--- a/gcc/ada/libgnat/s-valuti.adb
+++ b/gcc/ada/libgnat/s-valuti.adb
@@ -29,15 +29,27 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
+--  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);
+
 with System.Case_Util; use System.Case_Util;
 
-package body System.Val_Util is
+package body System.Val_Util
+  with SPARK_Mode
+is
 
    ---------------
    -- Bad_Value --
    ---------------
 
    procedure Bad_Value (S : String) is
+      pragma Annotate (GNATprove, Intentional, "exception might be raised",
+                       "Intentional exception from Bad_Value");
    begin
       --  Bad_Value might be called with very long strings allocated on the
       --  heap. Limit the size of the message so that we avoid creating a
@@ -62,21 +74,33 @@ package body System.Val_Util is
       F := S'First;
       L := S'Last;
 
+      --  Case of empty string
+
+      if F > L then
+         return;
+      end if;
+
       --  Scan for leading spaces
 
-      while F <= L and then S (F) = ' ' loop
+      while F < L and then S (F) = ' ' loop
+         pragma Loop_Invariant (F in S'First .. L - 1);
+         pragma Loop_Invariant (for all J in S'First .. F => S (J) = ' ');
          F := F + 1;
       end loop;
 
-      --  Case of no nonspace characters found
+      --  Case of no nonspace characters found. Decrease L to ensure L < F
+      --  without risking an overflow if F is Integer'Last.
 
-      if F > L then
+      if S (F) = ' ' then
+         L := L - 1;
          return;
       end if;
 
       --  Scan for trailing spaces
 
       while S (L) = ' ' loop
+         pragma Loop_Invariant (L in F + 1 .. S'Last);
+         pragma Loop_Invariant (for all J in L .. S'Last => S (J) = ' ');
          L := L - 1;
       end loop;
 
@@ -85,6 +109,8 @@ package body System.Val_Util is
       if S (F) /= ''' then
          for J in F .. L loop
             S (J) := To_Upper (S (J));
+            pragma Loop_Invariant
+              (for all K in F .. J => S (K) = To_Upper (S'Loop_Entry (K)));
          end loop;
       end if;
    end Normalize_String;
@@ -98,6 +124,8 @@ package body System.Val_Util is
       Ptr  : not null access Integer;
       Max  : Integer;
       Real : Boolean := False) return Integer
+   with
+     SPARK_Mode => Off  --  Function with side-effect through Ptr
    is
       P : Natural := Ptr.all;
       M : Boolean;
@@ -181,6 +209,8 @@ package body System.Val_Util is
       Ptr   : not null access Integer;
       Max   : Integer;
       Start : out Positive)
+   with
+     SPARK_Mode => Off  --  Not proved yet
    is
       P : Natural := Ptr.all;
 
@@ -226,6 +256,8 @@ package body System.Val_Util is
       Max   : Integer;
       Minus : out Boolean;
       Start : out Positive)
+   with
+     SPARK_Mode => Off  --  Not proved yet
    is
       P : Natural := Ptr.all;
 
@@ -283,7 +315,10 @@ package body System.Val_Util is
    -- Scan_Trailing_Blanks --
    --------------------------
 
-   procedure Scan_Trailing_Blanks (Str : String; P : Positive) is
+   procedure Scan_Trailing_Blanks (Str : String; P : Positive)
+   with
+     SPARK_Mode => Off  --  Not proved yet
+   is
    begin
       for J in P .. Str'Last loop
          if Str (J) /= ' ' then
@@ -302,6 +337,8 @@ package body System.Val_Util is
       Ptr : not null access Integer;
       Max : Integer;
       Ext : Boolean)
+   with
+     SPARK_Mode => Off  --  Not proved yet
    is
       C : Character;
 
diff --git a/gcc/ada/libgnat/s-valuti.ads b/gcc/ada/libgnat/s-valuti.ads
index 3d426d9..3223707 100644
--- a/gcc/ada/libgnat/s-valuti.ads
+++ b/gcc/ada/libgnat/s-valuti.ads
@@ -31,16 +31,60 @@
 
 --  This package provides some common utilities used by the s-valxxx files
 
-package System.Val_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.
 
-   procedure Bad_Value (S : String);
+pragma Assertion_Policy (Pre            => Ignore,
+                         Post           => Ignore,
+                         Contract_Cases => Ignore,
+                         Ghost          => Ignore);
+
+with System.Case_Util;
+
+package System.Val_Util
+  with SPARK_Mode, Pure
+is
+
+   procedure Bad_Value (S : String)
+   with
+     Depends => (null => S);
    pragma No_Return (Bad_Value);
    --  Raises constraint error with message: bad input for 'Value: "xxx"
 
+   function Only_Space_Ghost (S : String; From, To : Integer) return Boolean is
+      (for all J in From .. To => S (J) = ' ')
+   with
+     Ghost,
+     Pre => From > To or else (From >= S'First and then To <= S'Last);
+   --  Ghost function that returns True if S has only space characters from
+   --  index From to index To.
+
    procedure Normalize_String
      (S    : in out String;
-      F, L : out Integer);
+      F, L : out Integer)
+   with
+     Post => (if Only_Space_Ghost (S'Old, S'First, S'Last) then
+                F > L
+              else
+                F >= S'First
+                  and then L <= S'Last
+                  and then F <= L
+                  and then Only_Space_Ghost (S'Old, S'First, F - 1)
+                  and then S'Old (F) /= ' '
+                  and then S'Old (L) /= ' '
+                  and then
+                    (if L < S'Last then
+                      Only_Space_Ghost (S'Old, L + 1, S'Last))
+                  and then
+                    (if S'Old (F) /= ''' then
+                      (for all J in S'Range =>
+                        (if J in F .. L then
+                           S (J) = System.Case_Util.To_Upper (S'Old (J))
+                         else
+                           S (J) = S'Old (J)))));
    --  This procedure scans the string S setting F to be the index of the first
    --  non-blank character of S and L to be the index of the last non-blank
    --  character of S. Any lower case characters present in S will be folded to
@@ -85,7 +129,9 @@ package System.Val_Util is
      (Str  : String;
       Ptr  : not null access Integer;
       Max  : Integer;
-      Real : Boolean := False) return Integer;
+      Real : Boolean := False) return Integer
+   with
+     SPARK_Mode => Off;  --  Function with side-effect through Ptr
    --  Called to scan a possible exponent. Str, Ptr, Max are as described above
    --  for Scan_Sign. If Ptr.all < Max and Str (Ptr.all) = 'E' or 'e', then an
    --  exponent is scanned out, with the exponent value returned in Exp, and