Pre and postconditions in the formal containers library are
designed for formal verification. In general, we do not want to
execute them.
Tested on x86_64-pc-linux-gnu, committed on trunk
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 --git a/gcc/ada/libgnat/a-cfdlli.ads b/gcc/ada/libgnat/a-cfdlli.ads
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
