+2013-10-10 Yannick Moy <moy@adacore.com>
+
+ * gnat_rm.texi, a-cfdlli.ads, a-cfhase.ads, a-cforma.ads, a-cfhama.ads,
+ a-cforse.ads, a-cofove.ads: Update comment and doc of formal containers
+
+2013-10-10 Ed Schonberg <schonberg@adacore.com>
+
+ * sem_ch13.adb (Analyze_Aspect_Specifications): For Pre/Post
+ conditions that apply to a subprogram body, preserve the placement
+ and order of the generated pragmas, which must appear before
+ other declarations in the body.
+
2013-10-10 Bob Duff <duff@adacore.com>
* gnat_ugn.texi: Add gnat2xml doc.
------------------------------------------------------------------------------
-- This spec is derived from Ada.Containers.Bounded_Doubly_Linked_Lists in the
--- Ada 2012 RM. The modifications are to facilitate formal proofs by making it
--- easier to express properties.
+-- Ada 2012 RM. The modifications are meant to facilitate formal proofs by
+-- making it easier to express properties, and by making the specification of
+-- this unit compatible with SPARK 2014. Note that the API of this unit may be
+-- subject to incompatible changes as SPARK 2014 evolves.
-- The modifications are:
-- function Left (Container : List; Position : Cursor) return List;
-- function Right (Container : List; Position : Cursor) return List;
--- See subprogram specifications that follow for details
+-- See subprogram specifications that follow for details.
generic
type Element_Type is private;
------------------------------------------------------------------------------
-- This spec is derived from package Ada.Containers.Bounded_Hashed_Maps in the
--- Ada 2012 RM. The modifications are to facilitate formal proofs by making it
--- easier to express properties.
+-- Ada 2012 RM. The modifications are meant to facilitate formal proofs by
+-- making it easier to express properties, and by making the specification of
+-- this unit compatible with SPARK 2014. Note that the API of this unit may be
+-- subject to incompatible changes as SPARK 2014 evolves.
-- The modifications are:
-- function Left (Container : Map; Position : Cursor) return Map;
-- function Right (Container : Map; Position : Cursor) return Map;
--- See detailed specifications for these subprograms
+-- See detailed specifications for these subprograms.
private with Ada.Containers.Hash_Tables;
------------------------------------------------------------------------------
-- This spec is derived from package Ada.Containers.Bounded_Hashed_Sets in the
--- Ada 2012 RM. The modifications are to facilitate formal proofs by making it
--- easier to express properties.
+-- Ada 2012 RM. The modifications are meant to facilitate formal proofs by
+-- making it easier to express properties, and by making the specification of
+-- this unit compatible with SPARK 2014. Note that the API of this unit may be
+-- subject to incompatible changes as SPARK 2014 evolves.
-- The modifications are:
-- function Left (Container : Set; Position : Cursor) return Set;
-- function Right (Container : Set; Position : Cursor) return Set;
--- See detailed specifications for these subprograms
+-- See detailed specifications for these subprograms.
private with Ada.Containers.Hash_Tables;
------------------------------------------------------------------------------
-- This spec is derived from package Ada.Containers.Bounded_Ordered_Maps in
--- the Ada 2012 RM. The modifications are to facilitate formal proofs by
--- making it easier to express properties.
+-- the Ada 2012 RM. The modifications are meant to facilitate formal proofs by
+-- making it easier to express properties, and by making the specification of
+-- this unit compatible with SPARK 2014. Note that the API of this unit may be
+-- subject to incompatible changes as SPARK 2014 evolves.
-- The modifications are:
-- function Left (Container : Map; Position : Cursor) return Map;
-- function Right (Container : Map; Position : Cursor) return Map;
--- See detailed specifications for these subprograms
+-- See detailed specifications for these subprograms.
private with Ada.Containers.Red_Black_Trees;
------------------------------------------------------------------------------
-- This spec is derived from package Ada.Containers.Bounded_Ordered_Sets in
--- the Ada 2012 RM. The modifications are to facilitate formal proofs by
--- making it easier to express properties.
+-- the Ada 2012 RM. The modifications are meant to facilitate formal proofs by
+-- making it easier to express properties, and by making the specification of
+-- this unit compatible with SPARK 2014. Note that the API of this unit may be
+-- subject to incompatible changes as SPARK 2014 evolves.
-- The modifications are:
-- function Left (Container : Set; Position : Cursor) return Set;
-- function Right (Container : Set; Position : Cursor) return Set;
--- See detailed specifications for these subprograms
+-- See detailed specifications for these subprograms.
private with Ada.Containers.Red_Black_Trees;
------------------------------------------------------------------------------
-- This spec is derived from package Ada.Containers.Bounded_Vectors in the Ada
--- 2012 RM. The modifications are to facilitate formal proofs by making it
--- easier to express properties.
+-- 2012 RM. The modifications are meant to facilitate formal proofs by making
+-- it easier to express properties, and by making the specification of this
+-- unit compatible with SPARK 2014. Note that the API of this unit may be
+-- subject to incompatible changes as SPARK 2014 evolves.
-- The modifications are:
-- function Left (Container : Vector; Position : Cursor) return Vector;
-- function Right (Container : Vector; Position : Cursor) return Vector;
--- Left returns a container containing all elements preceding Position
--- (excluded) in Container. Right returns a container containing all
--- elements following Position (included) in Container. These two new
--- functions are useful to express invariant properties in loops which
--- iterate over containers. Left returns the part of the container already
--- scanned and Right the part not scanned yet.
+-- See detailed specifications for these subprograms.
with Ada.Containers;
use Ada.Containers;
function Left (Container : Vector; Position : Cursor) return Vector with
Pre => Has_Element (Container, Position) or else Position = No_Element;
-
function Right (Container : Vector; Position : Cursor) return Vector with
Pre => Has_Element (Container, Position) or else Position = No_Element;
+ -- Left returns a container containing all elements preceding Position
+ -- (excluded) in Container. Right returns a container containing all
+ -- elements following Position (included) in Container. These two new
+ -- functions can be used to express invariant properties in loops which
+ -- iterate over containers. Left returns the part of the container already
+ -- scanned and Right the part not scanned yet.
private
@cindex Formal container for doubly linked lists
@noindent
-This child of @code{Ada.Containers} defines a modified version of the Ada 2005
-container for doubly linked lists, meant to facilitate formal verification of
-code using such containers.
+This child of @code{Ada.Containers} defines a modified version of the
+Ada 2005 container for doubly linked lists, meant to facilitate formal
+verification of code using such containers. The specification of this
+unit is compatible with SPARK 2014. Note that the API of this unit may
+be subject to incompatible changes as SPARK 2014 evolves.
@node Ada.Containers.Formal_Hashed_Maps (a-cfhama.ads)
@section @code{Ada.Containers.Formal_Hashed_Maps} (@file{a-cfhama.ads})
@cindex Formal container for hashed maps
@noindent
-This child of @code{Ada.Containers} defines a modified version of the Ada 2005
-container for hashed maps, meant to facilitate formal verification of
-code using such containers.
+This child of @code{Ada.Containers} defines a modified version of the
+Ada 2005 container for hashed maps, meant to facilitate formal
+verification of code using such containers. The specification of this
+unit is compatible with SPARK 2014. Note that the API of this unit may
+be subject to incompatible changes as SPARK 2014 evolves.
@node Ada.Containers.Formal_Hashed_Sets (a-cfhase.ads)
@section @code{Ada.Containers.Formal_Hashed_Sets} (@file{a-cfhase.ads})
@cindex Formal container for hashed sets
@noindent
-This child of @code{Ada.Containers} defines a modified version of the Ada 2005
-container for hashed sets, meant to facilitate formal verification of
-code using such containers.
+This child of @code{Ada.Containers} defines a modified version of the
+Ada 2005 container for hashed sets, meant to facilitate formal
+verification of code using such containers. The specification of this
+unit is compatible with SPARK 2014. Note that the API of this unit may
+be subject to incompatible changes as SPARK 2014 evolves.
@node Ada.Containers.Formal_Ordered_Maps (a-cforma.ads)
@section @code{Ada.Containers.Formal_Ordered_Maps} (@file{a-cforma.ads})
@cindex Formal container for ordered maps
@noindent
-This child of @code{Ada.Containers} defines a modified version of the Ada 2005
-container for ordered maps, meant to facilitate formal verification of
-code using such containers.
+This child of @code{Ada.Containers} defines a modified version of the
+Ada 2005 container for ordered maps, meant to facilitate formal
+verification of code using such containers. The specification of this
+unit is compatible with SPARK 2014. Note that the API of this unit may
+be subject to incompatible changes as SPARK 2014 evolves.
@node Ada.Containers.Formal_Ordered_Sets (a-cforse.ads)
@section @code{Ada.Containers.Formal_Ordered_Sets} (@file{a-cforse.ads})
@cindex Formal container for ordered sets
@noindent
-This child of @code{Ada.Containers} defines a modified version of the Ada 2005
-container for ordered sets, meant to facilitate formal verification of
-code using such containers.
+This child of @code{Ada.Containers} defines a modified version of the
+Ada 2005 container for ordered sets, meant to facilitate formal
+verification of code using such containers. The specification of this
+unit is compatible with SPARK 2014. Note that the API of this unit may
+be subject to incompatible changes as SPARK 2014 evolves.
@node Ada.Containers.Formal_Vectors (a-cofove.ads)
@section @code{Ada.Containers.Formal_Vectors} (@file{a-cofove.ads})
@cindex Formal container for vectors
@noindent
-This child of @code{Ada.Containers} defines a modified version of the Ada 2005
-container for vectors, meant to facilitate formal verification of
-code using such containers.
+This child of @code{Ada.Containers} defines a modified version of the
+Ada 2005 container for vectors, meant to facilitate formal
+verification of code using such containers. The specification of this
+unit is compatible with SPARK 2014. Note that the API of this unit may
+be subject to incompatible changes as SPARK 2014 evolves.
@node Ada.Command_Line.Environment (a-colien.ads)
@section @code{Ada.Command_Line.Environment} (@file{a-colien.ads})
elsif Nkind (N) = N_Subprogram_Body then
if No (Declarations (N)) then
- Set_Declarations (N, New_List);
- end if;
+ Set_Declarations (N, New_List (Prag));
+ else
+ declare
+ D : Node_Id;
+ begin
+
+ -- There may be several aspects associated with the body;
+ -- preserve the ordering of the corresponding pragmas.
+
+ D := First (Declarations (N));
+ while Present (D) loop
+ exit when Nkind (D) /= N_Pragma
+ or else not From_Aspect_Specification (D);
+ Next (D);
+ end loop;
- Append (Prag, Declarations (N));
+ if No (D) then
+ Append (Prag, Declarations (N));
+ else
+ Insert_Before (D, Prag);
+ end if;
+ end;
+ end if;
-- Default
end;
end if;
+ -- Otherwise, Convention must be specified
+
Error_Msg_N
("missing Convention aspect for Export/Import",
Aspect);
projects / platform / upstream / linaro-gcc.git / commitdiff