ada: Activate SPARK_Mode in Ada.Numerics.*_Random specs

gcc/ada/ChangeLog:

	* libgnat/a-nudira.ads: Activate SPARK mode and add missing
	basic contracts. Mark the unit as always terminating.
	* libgnat/a-nuflra.ads: Idem.

diff --git a/gcc/ada/libgnat/a-nudira.ads b/gcc/ada/libgnat/a-nudira.ads
index 647470b7890ec51c0882601960f677e4e7bd1dea..3b2ca1868e8dbe917a02d6f079d9b97c58cd265e 100644 (file)
--- a/gcc/ada/libgnat/a-nudira.ads
+++ b/gcc/ada/libgnat/a-nudira.ads
@@ -44,38 +44,60 @@ generic
    type Result_Subtype is (<>);
 
 package Ada.Numerics.Discrete_Random with
-  SPARK_Mode => Off
+  SPARK_Mode => On,
+  Always_Terminates
 is
 
    --  Basic facilities
 
-   type Generator is limited private;
+   type Generator is limited private with Default_Initial_Condition;
 
-   function Random (Gen : Generator) return Result_Subtype;
+   function Random (Gen : Generator) return Result_Subtype with
+     Global => null,
+     Side_Effects;
+   pragma Annotate (GNATprove, Mutable_In_Parameters, Generator);
 
    function Random
      (Gen   : Generator;
       First : Result_Subtype;
       Last  : Result_Subtype) return Result_Subtype
-     with Post => Random'Result in First .. Last;
+     with
+       Post => Random'Result in First .. Last,
+       Global => null,
+       Side_Effects;
+   pragma Annotate (GNATprove, Mutable_In_Parameters, Generator);
 
-   procedure Reset (Gen : Generator; Initiator : Integer);
-   procedure Reset (Gen : Generator);
+   procedure Reset (Gen : Generator; Initiator : Integer) with
+     Global => null;
+   pragma Annotate (GNATprove, Mutable_In_Parameters, Generator);
+
+   procedure Reset (Gen : Generator) with
+     Global => null;
+   pragma Annotate (GNATprove, Mutable_In_Parameters, Generator);
 
    --  Advanced facilities
 
    type State is private;
 
-   procedure Save  (Gen : Generator; To_State   : out State);
-   procedure Reset (Gen : Generator; From_State : State);
+   procedure Save  (Gen : Generator; To_State   : out State) with
+     Global => null;
+   pragma Annotate (GNATprove, Mutable_In_Parameters, Generator);
+
+   procedure Reset (Gen : Generator; From_State : State) with
+     Global => null;
+   pragma Annotate (GNATprove, Mutable_In_Parameters, Generator);
 
    Max_Image_Width : constant := System.Random_Numbers.Max_Image_Width;
 
-   function Image (Of_State    : State)  return String;
-   function Value (Coded_State : String) return State;
+   function Image (Of_State    : State)  return String with
+     Global => null;
+   function Value (Coded_State : String) return State with
+     Global => null;
 
 private
 
+   pragma SPARK_Mode (Off);
+
    type Generator is new System.Random_Numbers.Generator;
 
    type State is new System.Random_Numbers.State;

diff --git a/gcc/ada/libgnat/a-nuflra.ads b/gcc/ada/libgnat/a-nuflra.ads
index 7eb0494bded09a96fc425f4037c79e3a18819433..9ea73d432a6fcf4d411e0e2e1bf9ed824276a064 100644 (file)
--- a/gcc/ada/libgnat/a-nuflra.ads
+++ b/gcc/ada/libgnat/a-nuflra.ads
@@ -39,34 +39,50 @@
 with System.Random_Numbers;
 
 package Ada.Numerics.Float_Random with
-  SPARK_Mode => Off
+  SPARK_Mode => On,
+  Always_Terminates
 is
 
    --  Basic facilities
 
-   type Generator is limited private;
+   type Generator is limited private with Default_Initial_Condition;
 
    subtype Uniformly_Distributed is Float range 0.0 .. 1.0;
 
-   function Random (Gen : Generator) return Uniformly_Distributed;
+   function Random (Gen : Generator) return Uniformly_Distributed with
+     Global => null,
+     Side_Effects;
+   pragma Annotate (GNATprove, Mutable_In_Parameters, Generator);
+   procedure Reset (Gen : Generator) with
+     Global => null;
+   pragma Annotate (GNATprove, Mutable_In_Parameters, Generator);
 
-   procedure Reset (Gen : Generator);
-   procedure Reset (Gen : Generator; Initiator : Integer);
+   procedure Reset (Gen : Generator; Initiator : Integer) with
+     Global => null;
+   pragma Annotate (GNATprove, Mutable_In_Parameters, Generator);
 
    --  Advanced facilities
 
    type State is private;
 
-   procedure Save  (Gen : Generator; To_State   : out State);
-   procedure Reset (Gen : Generator; From_State : State);
+   procedure Save  (Gen : Generator; To_State   : out State) with
+     Global => null;
+   pragma Annotate (GNATprove, Mutable_In_Parameters, Generator);
+   procedure Reset (Gen : Generator; From_State : State) with
+     Global => null;
+   pragma Annotate (GNATprove, Mutable_In_Parameters, Generator);
 
    Max_Image_Width : constant := System.Random_Numbers.Max_Image_Width;
 
-   function Image (Of_State    : State)  return String;
-   function Value (Coded_State : String) return State;
+   function Image (Of_State    : State)  return String with
+     Global => null;
+   function Value (Coded_State : String) return State with
+     Global => null;
 
 private
 
+   pragma SPARK_Mode (Off);
+
    type Generator is new System.Random_Numbers.Generator;
 
    type State is new System.Random_Numbers.State;