[gcc r12-1891] [Ada] Disable Pre/Post in formal containers

[Pierre-Marie de Rodat]

https://gcc.gnu.org/g:23a5c0fe8abc2f823be049a991eafe36fd31f5d7

commit r12-1891-g23a5c0fe8abc2f823be049a991eafe36fd31f5d7
Author: Claire Dross <dross@adacore.com>
Date:   Mon Apr 12 09:48:48 2021 +0200

    [Ada] Disable Pre/Post in formal containers
    
    gcc/ada/
    
            * libgnat/a-cfdlli.ads: Use pragma Assertion_Policy to disable
            pre and postconditions.
            * libgnat/a-cfhama.ads: Likewise.
            * libgnat/a-cfhase.ads: Likewise.
            * libgnat/a-cfinve.ads: Likewise.
            * libgnat/a-cforma.ads: Likewise.
            * libgnat/a-cforse.ads: Likewise.
            * libgnat/a-cofove.ads: Likewise.

Diff:
---
 gcc/ada/libgnat/a-cfdlli.ads | 5 +++++
 gcc/ada/libgnat/a-cfhama.ads | 5 +++++
 gcc/ada/libgnat/a-cfhase.ads | 5 +++++
 gcc/ada/libgnat/a-cfinve.ads | 5 +++++
 gcc/ada/libgnat/a-cforma.ads | 5 +++++
 gcc/ada/libgnat/a-cforse.ads | 5 +++++
 gcc/ada/libgnat/a-cofove.ads | 5 +++++
 7 files changed, 35 insertions(+)

diff --git a/gcc/ada/libgnat/a-cfdlli.ads b/gcc/ada/libgnat/a-cfdlli.ads
index d3bc3ba22a3..e3a2de6abd4 100644
--- a/gcc/ada/libgnat/a-cfdlli.ads
+++ b/gcc/ada/libgnat/a-cfdlli.ads
@@ -39,6 +39,11 @@ generic
 package Ada.Containers.Formal_Doubly_Linked_Lists with
   SPARK_Mode
 is
+   --  Contracts in this unit are meant for analysis only, not for run-time
+   --  checking.
+
+   pragma Assertion_Policy (Pre => Ignore);
+   pragma Assertion_Policy (Post => Ignore);
    pragma Annotate (CodePeer, Skip_Analysis);
 
    type List (Capacity : Count_Type) is private with
diff --git a/gcc/ada/libgnat/a-cfhama.ads b/gcc/ada/libgnat/a-cfhama.ads
index 9ccd9c2c409..e9b02682fda 100644
--- a/gcc/ada/libgnat/a-cfhama.ads
+++ b/gcc/ada/libgnat/a-cfhama.ads
@@ -64,6 +64,11 @@ generic
 package Ada.Containers.Formal_Hashed_Maps with
   SPARK_Mode
 is
+   --  Contracts in this unit are meant for analysis only, not for run-time
+   --  checking.
+
+   pragma Assertion_Policy (Pre => Ignore);
+   pragma Assertion_Policy (Post => Ignore);
    pragma Annotate (CodePeer, Skip_Analysis);
 
    type Map (Capacity : Count_Type; Modulus : Hash_Type) is private with
diff --git a/gcc/ada/libgnat/a-cfhase.ads b/gcc/ada/libgnat/a-cfhase.ads
index 47aaf0d5cf8..5d578632a05 100644
--- a/gcc/ada/libgnat/a-cfhase.ads
+++ b/gcc/ada/libgnat/a-cfhase.ads
@@ -62,6 +62,11 @@ generic
 package Ada.Containers.Formal_Hashed_Sets with
   SPARK_Mode
 is
+   --  Contracts in this unit are meant for analysis only, not for run-time
+   --  checking.
+
+   pragma Assertion_Policy (Pre => Ignore);
+   pragma Assertion_Policy (Post => Ignore);
    pragma Annotate (CodePeer, Skip_Analysis);
 
    type Set (Capacity : Count_Type; Modulus : Hash_Type) is private with
diff --git a/gcc/ada/libgnat/a-cfinve.ads b/gcc/ada/libgnat/a-cfinve.ads
index a8aeaa2c438..37dde920137 100644
--- a/gcc/ada/libgnat/a-cfinve.ads
+++ b/gcc/ada/libgnat/a-cfinve.ads
@@ -55,6 +55,11 @@ generic
 package Ada.Containers.Formal_Indefinite_Vectors with
   SPARK_Mode => On
 is
+   --  Contracts in this unit are meant for analysis only, not for run-time
+   --  checking.
+
+   pragma Assertion_Policy (Pre => Ignore);
+   pragma Assertion_Policy (Post => Ignore);
    pragma Annotate (CodePeer, Skip_Analysis);
 
    subtype Extended_Index is Index_Type'Base
diff --git a/gcc/ada/libgnat/a-cforma.ads b/gcc/ada/libgnat/a-cforma.ads
index 4e17978d361..d32727ea996 100644
--- a/gcc/ada/libgnat/a-cforma.ads
+++ b/gcc/ada/libgnat/a-cforma.ads
@@ -63,6 +63,11 @@ generic
 package Ada.Containers.Formal_Ordered_Maps with
   SPARK_Mode
 is
+   --  Contracts in this unit are meant for analysis only, not for run-time
+   --  checking.
+
+   pragma Assertion_Policy (Pre => Ignore);
+   pragma Assertion_Policy (Post => Ignore);
    pragma Annotate (CodePeer, Skip_Analysis);
 
    function Equivalent_Keys (Left, Right : Key_Type) return Boolean with
diff --git a/gcc/ada/libgnat/a-cforse.ads b/gcc/ada/libgnat/a-cforse.ads
index 61a93a3dd54..12d2d3c4758 100644
--- a/gcc/ada/libgnat/a-cforse.ads
+++ b/gcc/ada/libgnat/a-cforse.ads
@@ -59,6 +59,11 @@ generic
 package Ada.Containers.Formal_Ordered_Sets with
   SPARK_Mode
 is
+   --  Contracts in this unit are meant for analysis only, not for run-time
+   --  checking.
+
+   pragma Assertion_Policy (Pre => Ignore);
+   pragma Assertion_Policy (Post => Ignore);
    pragma Annotate (CodePeer, Skip_Analysis);
 
    function Equivalent_Elements (Left, Right : Element_Type) return Boolean
diff --git a/gcc/ada/libgnat/a-cofove.ads b/gcc/ada/libgnat/a-cofove.ads
index 217032f5174..61115ddc467 100644
--- a/gcc/ada/libgnat/a-cofove.ads
+++ b/gcc/ada/libgnat/a-cofove.ads
@@ -45,6 +45,11 @@ generic
 package Ada.Containers.Formal_Vectors with
   SPARK_Mode
 is
+   --  Contracts in this unit are meant for analysis only, not for run-time
+   --  checking.
+
+   pragma Assertion_Policy (Pre => Ignore);
+   pragma Assertion_Policy (Post => Ignore);
    pragma Annotate (CodePeer, Skip_Analysis);
 
    subtype Extended_Index is Index_Type'Base