Skip to content

R
riscv-gcc-1
Commit 2fc07285 by Arnaud Charlet
Options

[multiple changes] 

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.

From-SVN: r203347
parent c1645ac8
Showing with 102 additions and 45 deletions
gcc/ada/ChangeLog
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.
......
gcc/ada/a-cfdlli.ads
......@@ -30,8 +30,10 @@
------------------------------------------------------------------------------
-- 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:
......@@ -49,7 +51,7 @@
-- 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;
......
gcc/ada/a-cfhama.ads
......@@ -30,8 +30,10 @@
------------------------------------------------------------------------------
-- 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:
......@@ -49,7 +51,7 @@
-- 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;
......
gcc/ada/a-cfhase.ads
......@@ -30,8 +30,10 @@
------------------------------------------------------------------------------
-- 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:
......@@ -49,7 +51,7 @@
-- 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;
......
gcc/ada/a-cforma.ads
......@@ -30,8 +30,10 @@
------------------------------------------------------------------------------
-- 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:
......@@ -51,7 +53,7 @@
-- 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;
......
gcc/ada/a-cforse.ads
......@@ -30,8 +30,10 @@
------------------------------------------------------------------------------
-- 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:
......@@ -50,7 +52,7 @@
-- 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;
......
gcc/ada/a-cofove.ads
......@@ -30,8 +30,10 @@
------------------------------------------------------------------------------
-- 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:
......@@ -48,12 +50,7 @@
-- 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;
......@@ -350,9 +347,14 @@ package Ada.Containers.Formal_Vectors is
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
......
gcc/ada/gnat_rm.texi
......@@ -16995,9 +16995,11 @@ is specifically authorized by the Ada Reference Manual
@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})
......@@ -17005,9 +17007,11 @@ code using such containers.
@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})
......@@ -17015,9 +17019,11 @@ code using such containers.
@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})
......@@ -17025,9 +17031,11 @@ code using such containers.
@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})
......@@ -17035,9 +17043,11 @@ code using such containers.
@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})
......@@ -17045,9 +17055,11 @@ code using such containers.
@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})
......
gcc/ada/sem_ch13.adb
......@@ -1189,10 +1189,29 @@ package body Sem_Ch13 is
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
......@@ -2231,6 +2250,8 @@ package body Sem_Ch13 is
end;
end if;
-- Otherwise, Convention must be specified
Error_Msg_N
("missing Convention aspect for Export/Import",
Aspect);
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment