* [Ada] PR ada/105303 Fix use of Assertion_Policy in internal generics unit
@ 2022-05-30 8:32 Pierre-Marie de Rodat
0 siblings, 0 replies; only message in thread
From: Pierre-Marie de Rodat @ 2022-05-30 8:32 UTC (permalink / raw)
To: gcc-patches; +Cc: Yannick Moy
[-- Attachment #1: Type: text/plain, Size: 734 bytes --]
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.
[-- Attachment #2: patch.diff --]
[-- Type: text/x-diff, Size: 8827 bytes --]
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
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2022-05-30 8:32 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2022-05-30 8:32 [Ada] PR ada/105303 Fix use of Assertion_Policy in internal generics unit Pierre-Marie de Rodat
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).