diff mbox series

[COMMITTED] ada: Complete contracts of SPARK units

Message ID 20230526073645.2069721-1-poulhies@adacore.com
State Committed
Commit 81c360bd932b38e91b82b7a98f88e61c764b56ff
Headers
Series [COMMITTED] ada: Complete contracts of SPARK units |

Commit Message

Marc Poulhiès May 26, 2023, 7:36 a.m. UTC 
  From: Yannick Moy <moy@adacore.com>

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.

Tested on x86_64-pc-linux-gnu, committed on master.

---
 gcc/ada/libgnat/a-calend.ads |   8 +--
 gcc/ada/libgnat/a-ngelfu.ads |   6 ++
 gcc/ada/libgnat/a-textio.ads | 108 +++++++++++++++++++----------------
 gcc/ada/libgnat/i-cstrin.ads |  16 ++++--
 4 files changed, 80 insertions(+), 58 deletions(-)
diff mbox series

Patch

diff --git a/gcc/ada/libgnat/a-calend.ads b/gcc/ada/libgnat/a-calend.ads
index 2771cb5aa50..d67bf071c0e 100644
--- 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 f6d6c9643af..ae06ea710eb 100644
--- 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 713116e3e39..9cedab6a222 100644
--- 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 0f39cd8ed26..49b1f137270 100644
--- 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;