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
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
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
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
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
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
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