https://gcc.gnu.org/g:c657fe1488649a919f7cc48ea2b74c8aa062c5b8
commit r16-1163-gc657fe1488649a919f7cc48ea2b74c8aa062c5b8
Author: Andres Toom <t...@adacore.com>
Date: Tue Jan 28 15:41:27 2025 +0200
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:
---
gcc/ada/libgnat/a-nudira.ads | 42 ++++++++++++++++++++++++++++++++----------
gcc/ada/libgnat/a-nuflra.ads | 34 +++++++++++++++++++++++++---------
2 files changed, 57 insertions(+), 19 deletions(-)
diff --git a/gcc/ada/libgnat/a-nudira.ads b/gcc/ada/libgnat/a-nudira.ads
index 647470b7890e..3b2ca1868e8d 100644
--- 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 7eb0494bded0..9ea73d432a6f 100644
--- 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;
