diff mbox series

[Ada] PR ada/105303 Fix use of Assertion_Policy in internal generics unit

Message ID 20220530083237.GA210613@adacore.com
State New
Headers show
Series [Ada] PR ada/105303 Fix use of Assertion_Policy in internal generics unit | expand

Commit Message

Pierre-Marie de Rodat May 30, 2022, 8:32 a.m. UTC 
The internal unit System.Generic_Array_Operations defines only generic
subprograms. Thus, pragma Assertion_Policy inside the spec has no
effect, as each instantiation is only subject to the assertion policy at
the program point of the instantiation. Remove this confusing pragma,
and add the pragma inside each generic body making use of additional
assertions or ghost code, so that running time of instantiations is not
impacted by assertions meant for formal verification.

Tested on x86_64-pc-linux-gnu, committed on trunk

gcc/ada/

	PR ada/105303
	* libgnat/s-gearop.adb: Add pragma Assertion_Policy in generic
	bodies making use of additional assertions or ghost code.
	* libgnat/s-gearop.ads: Remove confusing Assertion_Policy.
diff mbox series

Patch

diff --git a/gcc/ada/libgnat/s-gearop.adb b/gcc/ada/libgnat/s-gearop.adb
--- a/gcc/ada/libgnat/s-gearop.adb
+++ b/gcc/ada/libgnat/s-gearop.adb
@@ -32,7 +32,8 @@ 
 --  Preconditions, postconditions, 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.
+--  policy to Ignore, here for non-generic code, and inside the generic for
+--  generic code.
 
 pragma Assertion_Policy (Pre            => Ignore,
                          Post           => Ignore,
@@ -72,6 +73,12 @@  is
    --------------
 
    function Diagonal (A : Matrix) return Vector is
+      pragma Assertion_Policy (Pre            => Ignore,
+                               Post           => Ignore,
+                               Ghost          => Ignore,
+                               Loop_Invariant => Ignore,
+                               Assert         => Ignore);
+
       N : constant Natural := Natural'Min (A'Length (1), A'Length (2));
    begin
       return R : Vector (A'First (1) .. A'First (1) + (N - 1))
@@ -126,6 +133,11 @@  is
    ---------------------
 
    procedure Back_Substitute (M, N : in out Matrix) is
+      pragma Assertion_Policy (Pre            => Ignore,
+                               Post           => Ignore,
+                               Ghost          => Ignore,
+                               Loop_Invariant => Ignore,
+                               Assert         => Ignore);
       pragma Assert (M'First (1) = N'First (1)
                        and then
                      M'Last  (1) = N'Last (1));
@@ -215,6 +227,11 @@  is
       N   : in out Matrix;
       Det : out Scalar)
    is
+      pragma Assertion_Policy (Pre            => Ignore,
+                               Post           => Ignore,
+                               Ghost          => Ignore,
+                               Loop_Invariant => Ignore,
+                               Assert         => Ignore);
       pragma Assert (M'First (1) = N'First (1)
                        and then
                      M'Last  (1) = N'Last (1));
@@ -460,6 +477,11 @@  is
    -------------
 
    function L2_Norm (X : X_Vector) return Result_Real'Base is
+      pragma Assertion_Policy (Pre            => Ignore,
+                               Post           => Ignore,
+                               Ghost          => Ignore,
+                               Loop_Invariant => Ignore,
+                               Assert         => Ignore);
       Sum : Result_Real'Base := 0.0;
 
    begin
@@ -479,6 +501,11 @@  is
    ----------------------------------
 
    function Matrix_Elementwise_Operation (X : X_Matrix) return Result_Matrix is
+      pragma Assertion_Policy (Pre            => Ignore,
+                               Post           => Ignore,
+                               Ghost          => Ignore,
+                               Loop_Invariant => Ignore,
+                               Assert         => Ignore);
    begin
       return R : Result_Matrix (X'Range (1), X'Range (2))
         with Relaxed_Initialization
@@ -524,6 +551,11 @@  is
      (Left  : Left_Matrix;
       Right : Right_Matrix) return Result_Matrix
    is
+      pragma Assertion_Policy (Pre            => Ignore,
+                               Post           => Ignore,
+                               Ghost          => Ignore,
+                               Loop_Invariant => Ignore,
+                               Assert         => Ignore);
    begin
       return R : Result_Matrix (Left'Range (1), Left'Range (2))
         with Relaxed_Initialization
@@ -570,6 +602,11 @@  is
       Y : Y_Matrix;
       Z : Z_Scalar) return Result_Matrix
    is
+      pragma Assertion_Policy (Pre            => Ignore,
+                               Post           => Ignore,
+                               Ghost          => Ignore,
+                               Loop_Invariant => Ignore,
+                               Assert         => Ignore);
    begin
       return R : Result_Matrix (X'Range (1), X'Range (2))
         with Relaxed_Initialization
@@ -657,6 +694,11 @@  is
      (Left  : Left_Matrix;
       Right : Right_Scalar) return Result_Matrix
    is
+      pragma Assertion_Policy (Pre            => Ignore,
+                               Post           => Ignore,
+                               Ghost          => Ignore,
+                               Loop_Invariant => Ignore,
+                               Assert         => Ignore);
    begin
       return R : Result_Matrix (Left'Range (1), Left'Range (2))
         with Relaxed_Initialization
@@ -705,6 +747,11 @@  is
      (Left  : Left_Scalar;
       Right : Right_Matrix) return Result_Matrix
    is
+      pragma Assertion_Policy (Pre            => Ignore,
+                               Post           => Ignore,
+                               Ghost          => Ignore,
+                               Loop_Invariant => Ignore,
+                               Assert         => Ignore);
    begin
       return R : Result_Matrix (Right'Range (1), Right'Range (2))
         with Relaxed_Initialization
@@ -811,6 +858,11 @@  is
      (Left  : Left_Matrix;
       Right : Right_Matrix) return Result_Matrix
    is
+      pragma Assertion_Policy (Pre            => Ignore,
+                               Post           => Ignore,
+                               Ghost          => Ignore,
+                               Loop_Invariant => Ignore,
+                               Assert         => Ignore);
    begin
       return R : Result_Matrix (Left'Range (1), Right'Range (2))
         with Relaxed_Initialization
@@ -856,6 +908,11 @@  is
    ----------------------------
 
    function Matrix_Vector_Solution (A : Matrix; X : Vector) return Vector is
+      pragma Assertion_Policy (Pre            => Ignore,
+                               Post           => Ignore,
+                               Ghost          => Ignore,
+                               Loop_Invariant => Ignore,
+                               Assert         => Ignore);
 
       procedure Ignore (M : Matrix)
       with
@@ -917,6 +974,11 @@  is
    ----------------------------
 
    function Matrix_Matrix_Solution (A, X : Matrix) return Matrix is
+      pragma Assertion_Policy (Pre            => Ignore,
+                               Post           => Ignore,
+                               Ghost          => Ignore,
+                               Loop_Invariant => Ignore,
+                               Assert         => Ignore);
 
       procedure Ignore (M : Matrix)
       with
@@ -1035,6 +1097,11 @@  is
      (Left  : Left_Vector;
       Right : Right_Vector) return Matrix
    is
+      pragma Assertion_Policy (Pre            => Ignore,
+                               Post           => Ignore,
+                               Ghost          => Ignore,
+                               Loop_Invariant => Ignore,
+                               Assert         => Ignore);
    begin
       return R : Matrix (Left'Range, Right'Range)
         with Relaxed_Initialization
@@ -1078,6 +1145,11 @@  is
    ---------------
 
    procedure Transpose (A : Matrix; R : out Matrix) is
+      pragma Assertion_Policy (Pre            => Ignore,
+                               Post           => Ignore,
+                               Ghost          => Ignore,
+                               Loop_Invariant => Ignore,
+                               Assert         => Ignore);
    begin
       for J in R'Range (1) loop
          for K in R'Range (2) loop


diff --git a/gcc/ada/libgnat/s-gearop.ads b/gcc/ada/libgnat/s-gearop.ads
--- a/gcc/ada/libgnat/s-gearop.ads
+++ b/gcc/ada/libgnat/s-gearop.ads
@@ -36,16 +36,10 @@ 
 --  overflows in arithmetic operations passed on as formal generic subprogram
 --  parameters.
 
---  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);
+--  Preconditions in this unit are meant mostly for analysis, but will be
+--  activated at runtime depending on the assertion policy for preconditions at
+--  the program point of instantiation. These preconditions are simply checking
+--  bounds, so should not impact running time.
 
 package System.Generic_Array_Operations
   with SPARK_Mode