[Ada] Proof of System.Val_Int at gold level

gcc/ada/

	* libgnat/s-valint.ads: Add SPARK_Mode and pragma to ignore
	assertions in instance and add additional ghost parameters to
	the instance of Value_I.
	* libgnat/s-vallli.ads: Idem.
	* libgnat/s-valllli.ads: Idem.
	* libgnat/s-valuei.ads, libgnat/s-valuei.adb: New generic
	parameters for ghost functions from System.Valueu. Add
	functional contracts.

5 files changed, 289 insertions, 22 deletions

diff --git a/gcc/ada/libgnat/s-valint.ads b/gcc/ada/libgnat/s-valint.ads
index 4fef265..c0d47aa 100644
--- a/gcc/ada/libgnat/s-valint.ads
+++ b/gcc/ada/libgnat/s-valint.ads
@@ -32,16 +32,39 @@
 --  This package contains routines for scanning signed Integer values for use
 --  in Text_IO.Integer_IO, and the Value attribute.
 
+--  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,
+                         Subprogram_Variant => Ignore);
+
 with System.Unsigned_Types;
 with System.Val_Uns;
 with System.Value_I;
 
-package System.Val_Int is
+package System.Val_Int with SPARK_Mode is
    pragma Preelaborate;
 
    subtype Unsigned is Unsigned_Types.Unsigned;
 
-   package Impl is new Value_I (Integer, Unsigned, Val_Uns.Scan_Raw_Unsigned);
+   package Impl is new Value_I
+     (Int                          => Integer,
+      Uns                          => Unsigned,
+      Scan_Raw_Unsigned            => Val_Uns.Scan_Raw_Unsigned,
+      Is_Raw_Unsigned_Format_Ghost =>
+         Val_Uns.Impl.Is_Raw_Unsigned_Format_Ghost,
+      Raw_Unsigned_Overflows_Ghost =>
+         Val_Uns.Impl.Raw_Unsigned_Overflows_Ghost,
+      Scan_Raw_Unsigned_Ghost      =>
+         Val_Uns.Impl.Scan_Raw_Unsigned_Ghost,
+      Raw_Unsigned_Last_Ghost      =>
+         Val_Uns.Impl.Raw_Unsigned_Last_Ghost);
 
    procedure Scan_Integer
      (Str : String;
diff --git a/gcc/ada/libgnat/s-vallli.ads b/gcc/ada/libgnat/s-vallli.ads
index ce1d9ee..dfb1729 100644
--- a/gcc/ada/libgnat/s-vallli.ads
+++ b/gcc/ada/libgnat/s-vallli.ads
@@ -32,19 +32,40 @@
 --  This package contains routines for scanning signed Long_Long_Integer
 --  values for use in Text_IO.Integer_IO, and the Value attribute.
 
+--  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,
+                         Subprogram_Variant => Ignore);
+
 with System.Unsigned_Types;
 with System.Val_LLU;
 with System.Value_I;
 
-package System.Val_LLI is
+package System.Val_LLI with SPARK_Mode is
    pragma Preelaborate;
 
    subtype Long_Long_Unsigned is Unsigned_Types.Long_Long_Unsigned;
 
-   package Impl is new
-     Value_I (Long_Long_Integer,
-              Long_Long_Unsigned,
-              Val_LLU.Scan_Raw_Long_Long_Unsigned);
+   package Impl is new Value_I
+     (Int                          => Long_Long_Integer,
+      Uns                          => Long_Long_Unsigned,
+      Scan_Raw_Unsigned            =>
+         Val_LLU.Scan_Raw_Long_Long_Unsigned,
+      Is_Raw_Unsigned_Format_Ghost =>
+         Val_LLU.Impl.Is_Raw_Unsigned_Format_Ghost,
+      Raw_Unsigned_Overflows_Ghost =>
+         Val_LLU.Impl.Raw_Unsigned_Overflows_Ghost,
+      Scan_Raw_Unsigned_Ghost      =>
+         Val_LLU.Impl.Scan_Raw_Unsigned_Ghost,
+      Raw_Unsigned_Last_Ghost      =>
+         Val_LLU.Impl.Raw_Unsigned_Last_Ghost);
 
    procedure Scan_Long_Long_Integer
      (Str  : String;
diff --git a/gcc/ada/libgnat/s-valllli.ads b/gcc/ada/libgnat/s-valllli.ads
index 176000a..84bca58 100644
--- a/gcc/ada/libgnat/s-valllli.ads
+++ b/gcc/ada/libgnat/s-valllli.ads
@@ -32,19 +32,40 @@
 --  This package contains routines for scanning signed Long_Long_Long_Integer
 --  values for use in Text_IO.Integer_IO, and the Value attribute.
 
+--  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,
+                         Subprogram_Variant => Ignore);
+
 with System.Unsigned_Types;
 with System.Val_LLLU;
 with System.Value_I;
 
-package System.Val_LLLI is
+package System.Val_LLLI with SPARK_Mode is
    pragma Preelaborate;
 
    subtype Long_Long_Long_Unsigned is Unsigned_Types.Long_Long_Long_Unsigned;
 
-   package Impl is new
-     Value_I (Long_Long_Long_Integer,
-              Long_Long_Long_Unsigned,
-              Val_LLLU.Scan_Raw_Long_Long_Long_Unsigned);
+   package Impl is new Value_I
+     (Int                          => Long_Long_Long_Integer,
+      Uns                          => Long_Long_Long_Unsigned,
+      Scan_Raw_Unsigned            =>
+         Val_LLLU.Scan_Raw_Long_Long_Long_Unsigned,
+      Is_Raw_Unsigned_Format_Ghost =>
+         Val_LLLU.Impl.Is_Raw_Unsigned_Format_Ghost,
+      Raw_Unsigned_Overflows_Ghost =>
+         Val_LLLU.Impl.Raw_Unsigned_Overflows_Ghost,
+      Scan_Raw_Unsigned_Ghost      =>
+         Val_LLLU.Impl.Scan_Raw_Unsigned_Ghost,
+      Raw_Unsigned_Last_Ghost      =>
+         Val_LLLU.Impl.Raw_Unsigned_Last_Ghost);
 
    procedure Scan_Long_Long_Long_Integer
      (Str  : String;
diff --git a/gcc/ada/libgnat/s-valuei.adb b/gcc/ada/libgnat/s-valuei.adb
index 83828d3..faf5791 100644
--- a/gcc/ada/libgnat/s-valuei.adb
+++ b/gcc/ada/libgnat/s-valuei.adb
@@ -29,10 +29,18 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
-with System.Val_Util; use System.Val_Util;
-
 package body System.Value_I 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,
+                            Assert_And_Cut     => Ignore,
+                            Subprogram_Variant => Ignore);
+
    ------------------
    -- Scan_Integer --
    ------------------
@@ -46,26 +54,35 @@ package body System.Value_I is
       Uval : Uns;
       --  Unsigned result
 
-      Minus : Boolean := False;
+      Minus : Boolean;
       --  Set to True if minus sign is present, otherwise to False
 
-      Start : Positive;
+      Unused_Start : Positive;
       --  Saves location of first non-blank (not used in this case)
 
+      Non_Blank : constant Positive :=
+        First_Non_Space_Ghost (Str, Ptr.all, Max)
+      with Ghost;
+      Fst_Num   : constant Positive :=
+        (if Str (Non_Blank) in '+' | '-' then Non_Blank + 1
+         else Non_Blank)
+      with Ghost;
+
    begin
-      Scan_Sign (Str, Ptr, Max, Minus, Start);
+      Scan_Sign (Str, Ptr, Max, Minus, Unused_Start);
 
       if Str (Ptr.all) not in '0' .. '9' then
-         Ptr.all := Start;
+         Ptr.all := Unused_Start;
          Bad_Value (Str);
       end if;
 
       Scan_Raw_Unsigned (Str, Ptr, Max, Uval);
+      pragma Assert (Uval = Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max));
 
       --  Deal with overflow cases, and also with largest negative number
 
       if Uval > Uns (Int'Last) then
-         if Minus and then Uval = Uns (-(Int'First)) then
+         if Minus and then Uval = Uns (Int'Last) + 1 then
             Res := Int'First;
          else
             Bad_Value (Str);
@@ -106,9 +123,31 @@ package body System.Value_I is
          declare
             V : Int;
             P : aliased Integer := Str'First;
+
+            Non_Blank : constant Positive := First_Non_Space_Ghost
+              (Str, Str'First, Str'Last)
+            with Ghost;
+            Fst_Num   : constant Positive :=
+              (if Str (Non_Blank) in '+' | '-' then Non_Blank + 1
+               else Non_Blank)
+              with Ghost;
          begin
-            Scan_Integer (Str, P'Access, Str'Last, V);
+            pragma Assert
+              (Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last)));
+
+            declare
+               P_Acc : constant not null access Integer := P'Access;
+            begin
+               Scan_Integer (Str, P_Acc, Str'Last, V);
+            end;
+
+            pragma Assert
+              (P = Raw_Unsigned_Last_Ghost (Str, Fst_Num, Str'Last));
+
             Scan_Trailing_Blanks (Str, P);
+
+            pragma Assert
+              (Is_Value_Integer_Ghost (Slide_If_Necessary (Str), V));
             return V;
          end;
       end if;
diff --git a/gcc/ada/libgnat/s-valuei.ads b/gcc/ada/libgnat/s-valuei.ads
index e0a34d9..d6a78fd 100644
--- a/gcc/ada/libgnat/s-valuei.ads
+++ b/gcc/ada/libgnat/s-valuei.ads
@@ -32,6 +32,16 @@
 --  This package contains routines for scanning signed integer values for use
 --  in Text_IO.Integer_IO, and the Value attribute.
 
+pragma Assertion_Policy (Pre                => Ignore,
+                         Post               => Ignore,
+                         Contract_Cases     => Ignore,
+                         Ghost              => Ignore,
+                         Subprogram_Variant => Ignore);
+pragma Warnings (Off, "postcondition does not mention function result");
+--  True postconditions are used to avoid inlining for GNATprove
+
+with System.Val_Util; use System.Val_Util;
+
 generic
 
    type Int is range <>;
@@ -44,14 +54,86 @@ generic
            Max : Integer;
            Res : out Uns);
 
+   --  Additional parameters for ghost subprograms used inside contracts
+
+   with function Is_Raw_Unsigned_Format_Ghost (Str : String) return Boolean;
+   with function Raw_Unsigned_Overflows_Ghost
+          (Str      : String;
+           From, To : Integer)
+           return Boolean;
+   with function Scan_Raw_Unsigned_Ghost
+          (Str      : String;
+           From, To : Integer)
+           return Uns;
+   with function Raw_Unsigned_Last_Ghost
+          (Str      : String;
+           From, To : Integer)
+           return Positive;
+
 package System.Value_I is
    pragma Preelaborate;
 
+   function Uns_Is_Valid_Int (Minus : Boolean; Uval : Uns) return Boolean is
+     (if Minus then Uval <= Uns (Int'Last) + 1
+      else Uval <= Uns (Int'Last))
+   with Ghost,
+     Post => True;
+   --  Return True if Uval (or -Uval when Minus is True) is a valid number of
+   --  type Int.
+
+   function Is_Int_Of_Uns
+     (Minus : Boolean;
+      Uval  : Uns;
+      Val   : Int)
+      return Boolean
+   is
+     (if Minus and then Uval = Uns (Int'Last) + 1 then Val = Int'First
+      elsif Minus then Val = -(Int (Uval))
+      else Val = Int (Uval))
+   with Ghost,
+     Pre  => Uns_Is_Valid_Int (Minus, Uval),
+     Post => True;
+   --  Return True if Uval (or -Uval when Minus is True) is equal to Val
+
    procedure Scan_Integer
      (Str : String;
       Ptr : not null access Integer;
       Max : Integer;
-      Res : out Int);
+      Res : out Int)
+   with
+     Pre  =>
+       Str'Last /= Positive'Last
+       --  Ptr.all .. Max is either an empty range, or a valid range in Str
+       and then (Ptr.all > Max
+                 or else (Ptr.all >= Str'First and then Max <= Str'Last))
+       and then not Only_Space_Ghost (Str, Ptr.all, Max)
+       and then
+         (declare
+            Non_Blank : constant Positive := First_Non_Space_Ghost
+              (Str, Ptr.all, Max);
+            Fst_Num   : constant Positive :=
+              (if Str (Non_Blank) in '+' | '-' then Non_Blank + 1
+               else Non_Blank);
+          begin
+            Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Max))
+            and then not Raw_Unsigned_Overflows_Ghost (Str, Fst_Num, Max)
+            and then Uns_Is_Valid_Int
+              (Minus => Str (Non_Blank) = '-',
+               Uval  => Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max))),
+    Post =>
+      (declare
+         Non_Blank : constant Positive := First_Non_Space_Ghost
+           (Str, Ptr.all'Old, Max);
+         Fst_Num   : constant Positive :=
+           (if Str (Non_Blank) in '+' | '-' then Non_Blank + 1
+            else Non_Blank);
+         Uval      : constant Uns :=
+            Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max);
+       begin
+           Is_Int_Of_Uns (Minus => Str (Non_Blank) = '-',
+                          Uval  => Uval,
+                          Val   => Res)
+             and then Ptr.all = Raw_Unsigned_Last_Ghost (Str, Fst_Num, Max));
    --  This procedure scans the string starting at Str (Ptr.all) for a valid
    --  integer according to the syntax described in (RM 3.5(43)). The substring
    --  scanned extends no further than Str (Max). There are three cases for the
@@ -77,10 +159,91 @@ package System.Value_I is
    --  special case of an all-blank string, and Ptr is unchanged, and hence
    --  is greater than Max as required in this case.
 
-   function Value_Integer (Str : String) return Int;
+   function Slide_To_1 (Str : String) return String
+   with Ghost,
+       Post =>
+         Only_Space_Ghost (Str, Str'First, Str'Last) =
+         (for all J in Str'First .. Str'Last =>
+            Slide_To_1'Result (J - Str'First + 1) = ' ');
+   --  Slides Str so that it starts at 1
+
+   function Slide_If_Necessary (Str : String) return String is
+     (if Str'Last = Positive'Last then Slide_To_1 (Str) else Str)
+   with Ghost,
+       Post =>
+         Only_Space_Ghost (Str, Str'First, Str'Last) =
+         Only_Space_Ghost (Slide_If_Necessary'Result,
+                           Slide_If_Necessary'Result'First,
+                           Slide_If_Necessary'Result'Last);
+   --  If Str'Last = Positive'Last then slides Str so that it starts at 1
+
+   function Is_Integer_Ghost (Str : String) return Boolean is
+     (declare
+        Non_Blank : constant Positive := First_Non_Space_Ghost
+          (Str, Str'First, Str'Last);
+        Fst_Num   : constant Positive :=
+          (if Str (Non_Blank) in '+' | '-' then Non_Blank + 1 else Non_Blank);
+      begin
+        Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last))
+        and then not Raw_Unsigned_Overflows_Ghost (Str, Fst_Num, Str'Last)
+        and then
+          Uns_Is_Valid_Int
+            (Minus => Str (Non_Blank) = '-',
+             Uval  => Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Str'Last))
+        and then Only_Space_Ghost
+           (Str, Raw_Unsigned_Last_Ghost (Str, Fst_Num, Str'Last), Str'Last))
+   with Ghost,
+       Pre => not Only_Space_Ghost (Str, Str'First, Str'Last)
+         and then Str'Last /= Positive'Last,
+       Post => True;
+   --  Ghost function that determines if Str has the correct format for a
+   --  signed number, consisting in some blank characters, an optional
+   --  sign, a raw unsigned number which does not overflow and then some
+   --  more blank characters.
+
+   function Is_Value_Integer_Ghost (Str : String; Val : Int) return Boolean is
+     (declare
+        Non_Blank : constant Positive := First_Non_Space_Ghost
+          (Str, Str'First, Str'Last);
+        Fst_Num   : constant Positive :=
+          (if Str (Non_Blank) in '+' | '-' then Non_Blank + 1 else Non_Blank);
+        Uval      : constant Uns :=
+          Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Str'Last);
+      begin
+        Is_Int_Of_Uns (Minus => Str (Non_Blank) = '-',
+                       Uval  => Uval,
+                       Val   => Val))
+   with Ghost,
+       Pre => not Only_Space_Ghost (Str, Str'First, Str'Last)
+         and then Str'Last /= Positive'Last
+         and then Is_Integer_Ghost (Str),
+       Post => True;
+   --  Ghost function that returns True if Val is the value corresponding to
+   --  the signed number represented by Str.
+
+   function Value_Integer (Str : String) return Int
+   with Pre => not Only_Space_Ghost (Str, Str'First, Str'Last)
+     and then Str'Length /= Positive'Last
+     and then Is_Integer_Ghost (Slide_If_Necessary (Str)),
+     Post =>
+         Is_Value_Integer_Ghost
+           (Slide_If_Necessary (Str), Value_Integer'Result),
+     Subprogram_Variant => (Decreases => Str'First);
    --  Used in computing X'Value (Str) where X is a signed integer type whose
    --  base range does not exceed the base range of Integer. Str is the string
    --  argument of the attribute. Constraint_Error is raised if the string is
    --  malformed, or if the value is out of range.
 
+private
+
+   ----------------
+   -- Slide_To_1 --
+   ----------------
+
+   function Slide_To_1 (Str : String) return String is
+      (declare
+         Res : constant String (1 .. Str'Length) := Str;
+       begin
+         Res);
+
 end System.Value_I;