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