From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: by sourceware.org (Postfix, from userid 1914) id 41EC83839C68; Mon, 30 May 2022 08:29:56 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 41EC83839C68 MIME-Version: 1.0 Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset="utf-8" From: Pierre-Marie de Rodat To: gcc-cvs@gcc.gnu.org Subject: [gcc r13-826] [Ada] PR ada/105303 Fix use of Assertion_Policy in internal generics unit X-Act-Checkin: gcc X-Git-Author: Yannick Moy X-Git-Refname: refs/heads/master X-Git-Oldrev: 55c19dda8c6c5fd40f1ec7ea4dd2f0c12d8c309f X-Git-Newrev: 5b7630f2f266346173eb2172a9a96e925010afc5 Message-Id: <20220530082956.41EC83839C68@sourceware.org> Date: Mon, 30 May 2022 08:29:56 +0000 (GMT) X-BeenThere: gcc-cvs@gcc.gnu.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: Gcc-cvs mailing list List-Unsubscribe: , List-Archive: List-Help: List-Subscribe: , X-List-Received-Date: Mon, 30 May 2022 08:29:56 -0000 https://gcc.gnu.org/g:5b7630f2f266346173eb2172a9a96e925010afc5 commit r13-826-g5b7630f2f266346173eb2172a9a96e925010afc5 Author: Yannick Moy Date: Tue Apr 19 14:37:58 2022 +0200 [Ada] PR ada/105303 Fix use of Assertion_Policy in internal generics unit 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. 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: --- gcc/ada/libgnat/s-gearop.adb | 74 +++++++++++++++++++++++++++++++++++++++++++- gcc/ada/libgnat/s-gearop.ads | 14 +++------ 2 files changed, 77 insertions(+), 11 deletions(-) diff --git a/gcc/ada/libgnat/s-gearop.adb b/gcc/ada/libgnat/s-gearop.adb index 32c67c320e5..78f4ba8b92f 100644 --- 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 index 15e11742ee4..f5ee8bc87e6 100644 --- 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