While the library of formal maps/sets correctly set SPARK_Mode on spec (On) and private part / body (Off), it was not the case for lists and vectors, thus causing some errors in GNATprove when instantiating such formal containers because bodies contain non-SPARK features (e.g. access types in formal vectors). Now fixed, which requires for formal lists and vectors that they are instantiated at library level, as other formal containers.
Tested on x86_64-pc-linux-gnu, committed on trunk 2014-11-20 Yannick Moy <m...@adacore.com> * a-cfdlli.adb, a-cfdlli.ads, a-cfinve.adb, a-cfinve.ads, * a-cofove.adb, a-cofove.ads: Mark spec as SPARK_Mode, and private part/body as SPARK_Mode Off. * a-cfhama.adb, a-cfhama.ads, a-cfhase.adb, a-cfhase.ads, * a-cforma.adb, a-cforma.ads, a-cforse.adb, a-cforse.ads: Use aspect instead of pragma for uniformity.
Index: a-cfdlli.adb =================================================================== --- a-cfdlli.adb (revision 217828) +++ a-cfdlli.adb (working copy) @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 2010-2013, Free Software Foundation, Inc. -- +-- Copyright (C) 2010-2014, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -27,7 +27,9 @@ with System; use type System.Address; -package body Ada.Containers.Formal_Doubly_Linked_Lists is +package body Ada.Containers.Formal_Doubly_Linked_Lists with + SPARK_Mode => Off +is ----------------------- -- Local Subprograms -- Index: a-cfdlli.ads =================================================================== --- a-cfdlli.ads (revision 217828) +++ a-cfdlli.ads (working copy) @@ -61,9 +61,11 @@ with function "=" (Left, Right : Element_Type) return Boolean is <>; -package Ada.Containers.Formal_Doubly_Linked_Lists is +package Ada.Containers.Formal_Doubly_Linked_Lists with + Pure, + SPARK_Mode +is pragma Annotate (GNATprove, External_Axiomatization); - pragma Pure; type List (Capacity : Count_Type) is private with Iterable => (First => First, @@ -337,6 +339,7 @@ -- scanned yet. private + pragma SPARK_Mode (Off); type Node_Type is record Prev : Count_Type'Base := -1; Index: a-cfhase.adb =================================================================== --- a-cfhase.adb (revision 217828) +++ a-cfhase.adb (working copy) @@ -35,8 +35,9 @@ with System; use type System.Address; -package body Ada.Containers.Formal_Hashed_Sets is - pragma SPARK_Mode (Off); +package body Ada.Containers.Formal_Hashed_Sets with + SPARK_Mode => Off +is ----------------------- -- Local Subprograms -- Index: a-cfhase.ads =================================================================== --- a-cfhase.ads (revision 217828) +++ a-cfhase.ads (working copy) @@ -67,10 +67,11 @@ with function "=" (Left, Right : Element_Type) return Boolean is <>; -package Ada.Containers.Formal_Hashed_Sets is +package Ada.Containers.Formal_Hashed_Sets with + Pure, + SPARK_Mode +is pragma Annotate (GNATprove, External_Axiomatization); - pragma Pure; - pragma SPARK_Mode (On); type Set (Capacity : Count_Type; Modulus : Hash_Type) is private with Iterable => (First => First, @@ -335,9 +336,10 @@ -- scanned yet. private - pragma Inline (Next); pragma SPARK_Mode (Off); + pragma Inline (Next); + type Node_Type is record Element : Element_Type; Index: a-cfinve.adb =================================================================== --- a-cfinve.adb (revision 217828) +++ a-cfinve.adb (working copy) @@ -26,7 +26,9 @@ -- <http://www.gnu.org/licenses/>. -- ------------------------------------------------------------------------------ -package body Ada.Containers.Formal_Indefinite_Vectors is +package body Ada.Containers.Formal_Indefinite_Vectors with + SPARK_Mode => Off +is function H (New_Item : Element_Type) return Holder renames To_Holder; function E (Container : Holder) return Element_Type renames Get; Index: a-cfinve.ads =================================================================== --- a-cfinve.ads (revision 217828) +++ a-cfinve.ads (working copy) @@ -52,7 +52,9 @@ -- size, and heap allocation will be avoided. If False, the containers can -- grow via heap allocation. -package Ada.Containers.Formal_Indefinite_Vectors is +package Ada.Containers.Formal_Indefinite_Vectors with + SPARK_Mode => On +is pragma Annotate (GNATprove, External_Axiomatization); subtype Extended_Index is Index_Type'Base @@ -220,6 +222,7 @@ Global => null; private + pragma SPARK_Mode (Off); pragma Inline (First_Index); pragma Inline (Last_Index); Index: a-cforma.adb =================================================================== --- a-cforma.adb (revision 217828) +++ a-cforma.adb (working copy) @@ -34,8 +34,9 @@ with System; use type System.Address; -package body Ada.Containers.Formal_Ordered_Maps is - pragma SPARK_Mode (Off); +package body Ada.Containers.Formal_Ordered_Maps with + SPARK_Mode => Off +is ----------------------------- -- Node Access Subprograms -- Index: a-cforma.ads =================================================================== --- a-cforma.ads (revision 217828) +++ a-cforma.ads (working copy) @@ -66,10 +66,11 @@ with function "<" (Left, Right : Key_Type) return Boolean is <>; with function "=" (Left, Right : Element_Type) return Boolean is <>; -package Ada.Containers.Formal_Ordered_Maps is +package Ada.Containers.Formal_Ordered_Maps with + Pure, + SPARK_Mode +is pragma Annotate (GNATprove, External_Axiomatization); - pragma Pure; - pragma SPARK_Mode (On); function Equivalent_Keys (Left, Right : Key_Type) return Boolean with Global => null; @@ -273,9 +274,10 @@ -- Overlap returns True if the containers have common keys private + pragma SPARK_Mode (Off); + pragma Inline (Next); pragma Inline (Previous); - pragma SPARK_Mode (Off); subtype Node_Access is Count_Type; Index: a-cfhama.adb =================================================================== --- a-cfhama.adb (revision 217828) +++ a-cfhama.adb (working copy) @@ -35,8 +35,9 @@ with System; use type System.Address; -package body Ada.Containers.Formal_Hashed_Maps is - pragma SPARK_Mode (Off); +package body Ada.Containers.Formal_Hashed_Maps with + SPARK_Mode => Off +is ----------------------- -- Local Subprograms -- Index: a-cfhama.ads =================================================================== --- a-cfhama.ads (revision 217828) +++ a-cfhama.ads (working copy) @@ -65,10 +65,11 @@ with function Equivalent_Keys (Left, Right : Key_Type) return Boolean; with function "=" (Left, Right : Element_Type) return Boolean is <>; -package Ada.Containers.Formal_Hashed_Maps is +package Ada.Containers.Formal_Hashed_Maps with + Pure, + SPARK_Mode +is pragma Annotate (GNATprove, External_Axiomatization); - pragma Pure; - pragma SPARK_Mode (On); type Map (Capacity : Count_Type; Modulus : Hash_Type) is private with Iterable => (First => First, @@ -272,6 +273,8 @@ -- Overlap returns True if the containers have common keys private + pragma SPARK_Mode (Off); + pragma Inline (Length); pragma Inline (Is_Empty); pragma Inline (Clear); @@ -282,7 +285,6 @@ pragma Inline (Has_Element); pragma Inline (Equivalent_Keys); pragma Inline (Next); - pragma SPARK_Mode (Off); type Node_Type is record Key : Key_Type; Index: a-cforse.adb =================================================================== --- a-cforse.adb (revision 217828) +++ a-cforse.adb (working copy) @@ -38,8 +38,9 @@ with System; use type System.Address; -package body Ada.Containers.Formal_Ordered_Sets is - pragma SPARK_Mode (Off); +package body Ada.Containers.Formal_Ordered_Sets with + SPARK_Mode => Off +is ------------------------------ -- Access to Fields of Node -- Index: a-cforse.ads =================================================================== --- a-cforse.ads (revision 217828) +++ a-cforse.ads (working copy) @@ -64,10 +64,11 @@ with function "<" (Left, Right : Element_Type) return Boolean is <>; with function "=" (Left, Right : Element_Type) return Boolean is <>; -package Ada.Containers.Formal_Ordered_Sets is +package Ada.Containers.Formal_Ordered_Sets with + Pure, + SPARK_Mode +is pragma Annotate (GNATprove, External_Axiomatization); - pragma Pure; - pragma SPARK_Mode (On); function Equivalent_Elements (Left, Right : Element_Type) return Boolean with @@ -353,9 +354,10 @@ -- scanned yet. private + pragma SPARK_Mode (Off); + pragma Inline (Next); pragma Inline (Previous); - pragma SPARK_Mode (Off); type Node_Type is record Has_Element : Boolean := False; Index: a-cofove.adb =================================================================== --- a-cofove.adb (revision 217828) +++ a-cofove.adb (working copy) @@ -30,7 +30,9 @@ with System; use type System.Address; -package body Ada.Containers.Formal_Vectors is +package body Ada.Containers.Formal_Vectors with + SPARK_Mode => Off +is Growth_Factor : constant := 2; -- When growing a container, multiply current capacity by this. Doubling Index: a-cofove.ads =================================================================== --- a-cofove.ads (revision 217828) +++ a-cofove.ads (working copy) @@ -46,7 +46,9 @@ -- size, and heap allocation will be avoided. If False, the containers can -- grow via heap allocation. -package Ada.Containers.Formal_Vectors is +package Ada.Containers.Formal_Vectors with + SPARK_Mode +is pragma Annotate (GNATprove, External_Axiomatization); subtype Extended_Index is Index_Type'Base @@ -230,6 +232,7 @@ -- scanned yet. private + pragma SPARK_Mode (Off); pragma Inline (First_Index); pragma Inline (Last_Index);