ada: Complete contracts of SPARK units

SPARK units in the standard library (both Ada and GNAT ones) should have
subprograms correctly annotated with contracts, so that a SPARK subprogram
should always return (not fail or raise an exception) under the conditions
expressed in its precondition, unless it is a procedure annotated with
Might_Not_Return.

gcc/ada/

	* libgnat/a-calend.ads: Mark with SPARK_Mode=>Off the functions which may
	raise Time_Error.
	* libgnat/a-ngelfu.ads: Mark with SPARK_Mode=>Off the functions which may
	lead to an overflow (which is not the case of Tan with one parameter for
	example, or Arctanh or Arcoth, despite their mathematical range covering
	the reals).
	* libgnat/a-textio.ads: Remove Always_Return annotation from functions, as
	this is now compulsory for functions to always return in SPARK.
	* libgnat/i-cstrin.ads: Add Might_Not_Return annotation to Update procedure
	which may not return.

diff --git a/gcc/ada/libgnat/a-calend.ads b/gcc/ada/libgnat/a-calend.ads
index 2771cb5aa50da6ffefc19a6e6b04c7a983222fb5..d67bf071c0ebd45a09e824678b2f0298cb25108f 100644 (file)
--- a/gcc/ada/libgnat/a-calend.ads
+++ b/gcc/ada/libgnat/a-calend.ads
@@ -102,16 +102,16 @@ is
 
    function "+" (Left : Time;     Right : Duration) return Time
    with
-     Global => null;
+     SPARK_Mode => Off;
    function "+" (Left : Duration; Right : Time)     return Time
    with
-     Global => null;
+     SPARK_Mode => Off;
    function "-" (Left : Time;     Right : Duration) return Time
    with
-     Global => null;
+     SPARK_Mode => Off;
    function "-" (Left : Time;     Right : Time)     return Duration
    with
-     Global => null;
+     SPARK_Mode => Off;
    --  The first three functions will raise Time_Error if the resulting time
    --  value is less than the start of Ada time in UTC or greater than the
    --  end of Ada time in UTC. The last function will raise Time_Error if the

diff --git a/gcc/ada/libgnat/a-ngelfu.ads b/gcc/ada/libgnat/a-ngelfu.ads
index f6d6c9643af9b9fb2daeb72746782e48c66bab09..ae06ea710ebfe86d5cfb8d5aef735cfff8e9f32d 100644 (file)
--- a/gcc/ada/libgnat/a-ngelfu.ads
+++ b/gcc/ada/libgnat/a-ngelfu.ads
@@ -116,14 +116,17 @@ is
      Post => (if X = 0.0 then Tan'Result = 0.0);
 
    function Tan (X, Cycle : Float_Type'Base) return Float_Type'Base with
+     SPARK_Mode => Off,  --  Tan can overflow for some values of X and Cycle
      Pre  => Cycle > 0.0
        and then abs Float_Type'Base'Remainder (X, Cycle) /= 0.25 * Cycle,
      Post => (if X = 0.0 then Tan'Result = 0.0);
 
    function Cot (X : Float_Type'Base) return Float_Type'Base with
+     SPARK_Mode => Off,  --  Cot can overflow for some values of X
      Pre => X /= 0.0;
 
    function Cot (X, Cycle : Float_Type'Base) return Float_Type'Base with
+     SPARK_Mode => Off,  --  Cot can overflow for some values of X and Cycle
      Pre => Cycle > 0.0
        and then X /= 0.0
        and then Float_Type'Base'Remainder (X, Cycle) /= 0.0
@@ -176,9 +179,11 @@ is
      Post => (if X > 0.0 and then Y = 0.0 then Arccot'Result = 0.0);
 
    function Sinh (X : Float_Type'Base) return Float_Type'Base with
+     SPARK_Mode => Off,  --  Sinh can overflow for some values of X
      Post => (if X = 0.0 then Sinh'Result = 0.0);
 
    function Cosh (X : Float_Type'Base) return Float_Type'Base with
+     SPARK_Mode => Off,  --  Cosh can overflow for some values of X
      Post => Cosh'Result >= 1.0
        and then (if X = 0.0 then Cosh'Result = 1.0);
 
@@ -187,6 +192,7 @@ is
        and then (if X = 0.0 then Tanh'Result = 0.0);
 
    function Coth (X : Float_Type'Base) return Float_Type'Base with
+     SPARK_Mode => Off,  --  Coth can overflow for some values of X
      Pre  => X /= 0.0,
      Post => abs Coth'Result >= 1.0;
 

diff --git a/gcc/ada/libgnat/a-textio.ads b/gcc/ada/libgnat/a-textio.ads
index 713116e3e39b9d2ca58f0f12b2e7db01ec26cd5c..9cedab6a22237fb860bb651fcdb95dd04e81c4c4 100644 (file)
--- a/gcc/ada/libgnat/a-textio.ads
+++ b/gcc/ada/libgnat/a-textio.ads
@@ -132,11 +132,13 @@ is
      Post     => not Is_Open (File),
      Global   => (In_Out => File_System),
      Annotate => (GNATprove, Always_Return);
+
    procedure Delete (File : in out File_Type) with
      Pre      => Is_Open (File),
      Post     => not Is_Open (File),
      Global   => (In_Out => File_System),
      Annotate => (GNATprove, Might_Not_Return);
+
    procedure Reset  (File : in out File_Type; Mode : File_Mode) with
      Pre      => Is_Open (File),
      Post     =>
@@ -147,6 +149,7 @@ is
                          and then Page_Length (File) = 0)),
      Global   => (In_Out => File_System),
      Annotate => (GNATprove, Might_Not_Return);
+
    procedure Reset  (File : in out File_Type) with
      Pre      => Is_Open (File),
      Post     =>
@@ -159,21 +162,19 @@ is
      Annotate => (GNATprove, Might_Not_Return);
 
    function Mode (File : File_Type) return File_Mode with
-     Pre      => Is_Open (File),
-     Global   => null,
-     Annotate => (GNATprove, Always_Return);
+     Pre    => Is_Open (File),
+     Global => null;
+
    function Name (File : File_Type) return String with
-     Pre      => Is_Open (File),
-     Global   => null,
-     Annotate => (GNATprove, Always_Return);
+     Pre    => Is_Open (File),
+     Global => null;
+
    function Form (File : File_Type) return String with
-     Pre      => Is_Open (File),
-     Global   => null,
-     Annotate => (GNATprove, Always_Return);
+     Pre    => Is_Open (File),
+     Global => null;
 
    function Is_Open (File : File_Type) return Boolean with
-     Global   => null,
-     Annotate => (GNATprove, Always_Return);
+     Global => null;
 
    ------------------------------------------------------
    -- Control of default input, output and error files --
@@ -215,6 +216,7 @@ is
        and Page_Length (File)'Old = Page_Length (File),
      Global   => (In_Out => File_System),
      Annotate => (GNATprove, Always_Return);
+
    procedure Flush with
      Post     =>
        Line_Length'Old = Line_Length
@@ -233,6 +235,7 @@ is
        and Page_Length (File)'Old = Page_Length (File),
      Global   => (In_Out => File_System),
      Annotate => (GNATprove, Might_Not_Return);
+
    procedure Set_Line_Length (To : Count) with
      Post     =>
        Line_Length = To
@@ -247,6 +250,7 @@ is
        and Line_Length (File)'Old = Line_Length (File),
      Global   => (In_Out => File_System),
      Annotate => (GNATprove, Might_Not_Return);
+
    procedure Set_Page_Length (To : Count) with
      Post     =>
        Page_Length = To
@@ -255,18 +259,18 @@ is
      Annotate => (GNATprove, Might_Not_Return);
 
    function Line_Length (File : File_Type) return Count with
-     Pre      => Is_Open (File) and then Mode (File) /= In_File,
-     Global   => (Input => File_System);
+     Pre    => Is_Open (File) and then Mode (File) /= In_File,
+     Global => (Input => File_System);
+
    function Line_Length return Count with
-     Global   => (Input => File_System),
-     Annotate => (GNATprove, Always_Return);
+     Global => (Input => File_System);
 
    function Page_Length (File : File_Type) return Count with
-     Pre      => Is_Open (File) and then Mode (File) /= In_File,
-     Global   => (Input => File_System);
+     Pre    => Is_Open (File) and then Mode (File) /= In_File,
+     Global => (Input => File_System);
+
    function Page_Length return Count with
-     Global   => (Input => File_System),
-     Annotate => (GNATprove, Always_Return);
+     Global => (Input => File_System);
 
    ------------------------------------
    -- Column, Line, and Page Control --
@@ -279,6 +283,7 @@ is
        and Page_Length (File)'Old = Page_Length (File),
      Global   => (In_Out => File_System),
      Annotate => (GNATprove, Always_Return);
+
    procedure New_Line (Spacing : Positive_Count := 1) with
      Post     =>
        Line_Length'Old = Line_Length
@@ -290,6 +295,7 @@ is
      Pre      => Is_Open (File) and then Mode (File) = In_File,
      Global   => (In_Out => File_System),
      Annotate => (GNATprove, Might_Not_Return);
+
    procedure Skip_Line (Spacing : Positive_Count := 1) with
      Post     =>
        Line_Length'Old = Line_Length
@@ -298,12 +304,11 @@ is
      Annotate => (GNATprove, Might_Not_Return);
 
    function End_Of_Line (File : File_Type) return Boolean with
-     Pre      => Is_Open (File) and then Mode (File) = In_File,
-     Global   => (Input => File_System),
-     Annotate => (GNATprove, Always_Return);
+     Pre    => Is_Open (File) and then Mode (File) = In_File,
+     Global => (Input => File_System);
+
    function End_Of_Line return Boolean with
-     Global   => (Input => File_System),
-     Annotate => (GNATprove, Always_Return);
+     Global => (Input => File_System);
 
    procedure New_Page (File : File_Type) with
      Pre      => Is_Open (File) and then Mode (File) /= In_File,
@@ -312,6 +317,7 @@ is
        and Page_Length (File)'Old = Page_Length (File),
      Global   => (In_Out => File_System),
      Annotate => (GNATprove, Always_Return);
+
    procedure New_Page with
      Post     =>
        Line_Length'Old = Line_Length
@@ -323,6 +329,7 @@ is
      Pre      => Is_Open (File) and then Mode (File) = In_File,
      Global   => (In_Out => File_System),
      Annotate => (GNATprove, Might_Not_Return);
+
    procedure Skip_Page with
      Post     =>
        Line_Length'Old = Line_Length
@@ -331,20 +338,18 @@ is
      Annotate => (GNATprove, Might_Not_Return);
 
    function End_Of_Page (File : File_Type) return Boolean with
-     Pre      => Is_Open (File) and then Mode (File) = In_File,
-     Global   => (Input => File_System),
-     Annotate => (GNATprove, Always_Return);
+     Pre    => Is_Open (File) and then Mode (File) = In_File,
+     Global => (Input => File_System);
+
    function End_Of_Page return Boolean with
-     Global   => (Input => File_System),
-     Annotate => (GNATprove, Always_Return);
+     Global => (Input => File_System);
 
    function End_Of_File (File : File_Type) return Boolean with
-     Pre      => Is_Open (File) and then Mode (File) = In_File,
-     Global   => (Input => File_System),
-     Annotate => (GNATprove, Always_Return);
+     Pre    => Is_Open (File) and then Mode (File) = In_File,
+     Global => (Input => File_System);
+
    function End_Of_File return Boolean with
-     Global   => (Input => File_System),
-     Annotate => (GNATprove, Always_Return);
+     Global => (Input => File_System);
 
    procedure Set_Col (File : File_Type;  To : Positive_Count) with
      Pre            =>
@@ -359,6 +364,7 @@ is
         others                 => True),
      Global         => (In_Out => File_System),
      Annotate       => (GNATprove, Might_Not_Return);
+
    procedure Set_Col (To : Positive_Count) with
      Pre      => Line_Length = 0 or To <= Line_Length,
      Post     =>
@@ -380,6 +386,7 @@ is
         others                 => True),
      Global         => (In_Out => File_System),
      Annotate       => (GNATprove, Might_Not_Return);
+
    procedure Set_Line (To : Positive_Count) with
      Pre      => Page_Length = 0 or To <= Page_Length,
      Post     =>
@@ -389,28 +396,25 @@ is
      Annotate => (GNATprove, Might_Not_Return);
 
    function Col (File : File_Type) return Positive_Count with
-     Pre      => Is_Open (File),
-     Global   => (Input => File_System),
-     Annotate => (GNATprove, Always_Return);
+     Pre    => Is_Open (File),
+     Global => (Input => File_System);
+
    function Col return Positive_Count with
-     Global   => (Input => File_System),
-     Annotate => (GNATprove, Always_Return);
+     Global => (Input => File_System);
 
    function Line (File : File_Type) return Positive_Count with
-     Pre      => Is_Open (File),
-     Global   => (Input => File_System),
-     Annotate => (GNATprove, Always_Return);
+     Pre    => Is_Open (File),
+     Global => (Input => File_System);
+
    function Line return Positive_Count with
-     Global   => (Input => File_System),
-     Annotate => (GNATprove, Always_Return);
+     Global => (Input => File_System);
 
    function Page (File : File_Type) return Positive_Count with
-     Pre      => Is_Open (File),
-     Global   => (Input => File_System),
-     Annotate => (GNATprove, Always_Return);
+     Pre    => Is_Open (File),
+     Global => (Input => File_System);
+
    function Page return Positive_Count with
-     Global   => (Input => File_System),
-     Annotate => (GNATprove, Always_Return);
+     Global => (Input => File_System);
 
    ----------------------------
    -- Character Input-Output --
@@ -420,12 +424,14 @@ is
      Pre      => Is_Open (File) and then Mode (File) = In_File,
      Global   => (In_Out => File_System),
      Annotate => (GNATprove, Might_Not_Return);
+
    procedure Get (Item : out Character) with
      Post   =>
        Line_Length'Old = Line_Length
        and Page_Length'Old = Page_Length,
      Global   => (In_Out => File_System),
      Annotate => (GNATprove, Might_Not_Return);
+
    procedure Put (File : File_Type; Item : Character) with
      Pre      => Is_Open (File) and then Mode (File) /= In_File,
      Post     =>
@@ -433,6 +439,7 @@ is
        and Page_Length (File)'Old = Page_Length (File),
      Global   => (In_Out => File_System),
      Annotate => (GNATprove, Always_Return);
+
    procedure Put (Item : Character) with
      Post     =>
        Line_Length'Old = Line_Length
@@ -503,12 +510,14 @@ is
      Pre      => Is_Open (File) and then Mode (File) = In_File,
      Global   => (In_Out => File_System),
      Annotate => (GNATprove, Might_Not_Return);
+
    procedure Get (Item : out String) with
      Post     =>
        Line_Length'Old = Line_Length
        and Page_Length'Old = Page_Length,
      Global   => (In_Out => File_System),
      Annotate => (GNATprove, Might_Not_Return);
+
    procedure Put (File : File_Type; Item : String) with
      Pre      => Is_Open (File) and then Mode (File) /= In_File,
      Post     =>
@@ -516,6 +525,7 @@ is
        and Page_Length (File)'Old = Page_Length (File),
      Global   => (In_Out => File_System),
      Annotate => (GNATprove, Always_Return);
+
    procedure Put (Item : String) with
      Post     =>
        Line_Length'Old = Line_Length

diff --git a/gcc/ada/libgnat/i-cstrin.ads b/gcc/ada/libgnat/i-cstrin.ads
index 0f39cd8ed26d6916c028ea7be191c0291e6df18e..49b1f137270096dcc3511d1b10a5a1380adde856 100644 (file)
--- a/gcc/ada/libgnat/i-cstrin.ads
+++ b/gcc/ada/libgnat/i-cstrin.ads
@@ -67,7 +67,7 @@ is
      (Item      : char_array_access;
       Nul_Check : Boolean := False) return chars_ptr
    with
-     SPARK_Mode => Off;
+     SPARK_Mode => Off;  --  To_Chars_Ptr'Result is aliased with Item
 
    function New_Char_Array (Chars : char_array) return chars_ptr with
      Volatile_Function,
@@ -118,13 +118,16 @@ is
       Chars  : char_array;
       Check  : Boolean := True)
    with
-     Pre    =>
+     Pre      =>
        Item /= Null_Ptr
          and then
       (if Check then
          Strlen (Item) <= size_t'Last - Offset
            and then Strlen (Item) + Offset <= Chars'Length),
-     Global => (In_Out => C_Memory);
+     Global   => (In_Out => C_Memory),
+     Annotate => (GNATprove, Might_Not_Return);
+     --  Update may not return if Check is False and the null terminator
+     --  is overwritten or skipped with Offset.
 
    procedure Update
      (Item   : chars_ptr;
@@ -132,13 +135,16 @@ is
       Str    : String;
       Check  : Boolean := True)
    with
-     Pre    =>
+     Pre      =>
        Item /= Null_Ptr
          and then
       (if Check then
          Strlen (Item) <= size_t'Last - Offset
            and then Strlen (Item) + Offset <= Str'Length),
-     Global => (In_Out => C_Memory);
+     Global   => (In_Out => C_Memory),
+     Annotate => (GNATprove, Might_Not_Return);
+     --  Update may not return if Check is False and the null terminator
+     --  is overwritten or skipped with Offset.
 
    Update_Error : exception;