2011-08-02 Claire Dross <dross@adacore.com>

	* a-cfdlli.ads, a-cfhase.ads, a-cforma.ads, a-cfhama.ads, a-cforse.ads,
	a-cofove.ads: Add comments.

2011-08-02  Yannick Moy  <moy@adacore.com>

	* gnat_rm.texi: Document formal containers.

2011-08-02  Emmanuel Briot  <briot@adacore.com>

	* g-comlin.adb (Goto_Section, Getopt): fix handling of "*" when there
	are empty sections.



git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@177111 138bc75d-0d04-0410-961f-82ee72b054a4

9 files changed, 266 insertions, 14 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index c6a2ff86f88..66995e3a36f 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,17 @@
+2011-08-02  Claire Dross  <dross@adacore.com>
+
+	* a-cfdlli.ads, a-cfhase.ads, a-cforma.ads, a-cfhama.ads, a-cforse.ads,
+	a-cofove.ads: Add comments.
+
+2011-08-02  Yannick Moy  <moy@adacore.com>
+
+	* gnat_rm.texi: Document formal containers.
+
+2011-08-02  Emmanuel Briot  <briot@adacore.com>
+
+	* g-comlin.adb (Goto_Section, Getopt): fix handling of "*" when there
+	are empty sections.
+
 2011-08-02  Robert Dewar  <dewar@adacore.com>
 
 	* mlib-prj.adb, restrict.ads, sem_aggr.adb, sem_ch12.adb: Minor
diff --git a/gcc/ada/a-cfdlli.ads b/gcc/ada/a-cfdlli.ads
index af64ea35f8b..526410c3b79 100644
--- a/gcc/ada/a-cfdlli.ads
+++ b/gcc/ada/a-cfdlli.ads
@@ -29,6 +29,30 @@
 -- <http://www.gnu.org/licenses/>.                                          --
 ------------------------------------------------------------------------------
 
+--  The specification of this package is derived from the specification
+--  of package Ada.Containers.Bounded_Doubly_Linked_Lists in the Ada 2012 RM.
+--  The changes are
+
+--    A parameter for the container is added to every function reading the
+--    content of a container: Element, Next, Previous, Query_Element,
+--    Has_Element, Iterate, Reverse_Iterate. This change is motivated by the
+--    need to have cursors which are valid on different containers (typically
+--    a container C and its previous version C'Old) for expressing properties,
+--    which is not possible if cursors encapsulate an access to the underlying
+--    container.
+
+--    There are two new functions
+
+--      function Left  (Container : List; Position : Cursor) return List;
+--      function Right (Container : List; Position : Cursor) return List;
+
+--      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.
+
 private with Ada.Streams;
 with Ada.Containers; use Ada.Containers;
 
diff --git a/gcc/ada/a-cfhama.ads b/gcc/ada/a-cfhama.ads
index 03b6d36789d..f11f5dac723 100644
--- a/gcc/ada/a-cfhama.ads
+++ b/gcc/ada/a-cfhama.ads
@@ -29,6 +29,30 @@
 -- <http://www.gnu.org/licenses/>.                                          --
 ------------------------------------------------------------------------------
 
+--  The specification of this package is derived from the specification
+--  of package Ada.Containers.Bounded_Hashed_Maps in the Ada 2012 RM.
+--  The changes are
+
+--    A parameter for the container is added to every function reading the
+--    content of a container: Key, Element, Next, Query_Element,
+--    Has_Element, Iterate, Equivalent_Keys. This change is motivated by the
+--    need to have cursors which are valid on different containers (typically
+--    a container C and its previous version C'Old) for expressing properties,
+--    which is not possible if cursors encapsulate an access to the underlying
+--    container.
+
+--    There are two new functions
+
+--      function Left  (Container : Map; Position : Cursor) return Map;
+--      function Right (Container : Map; Position : Cursor) return Map;
+
+--      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.
+
 private with Ada.Containers.Hash_Tables;
 private with Ada.Streams;
 with Ada.Containers; use Ada.Containers;
diff --git a/gcc/ada/a-cfhase.ads b/gcc/ada/a-cfhase.ads
index 2a6a613b3da..33c10c693f9 100644
--- a/gcc/ada/a-cfhase.ads
+++ b/gcc/ada/a-cfhase.ads
@@ -29,6 +29,30 @@
 -- <http://www.gnu.org/licenses/>.                                          --
 ------------------------------------------------------------------------------
 
+--  The specification of this package is derived from the specification
+--  of package Ada.Containers.Bounded_Hashed_Sets in the Ada 2012 RM.
+--  The changes are
+
+--    A parameter for the container is added to every function reading the
+--    content of a container: Element, Next, Query_Element, Has_Element,
+--    Key, Iterate, Equivalent_Elements. This change is motivated by the
+--    need to have cursors which are valid on different containers (typically
+--    a container C and its previous version C'Old) for expressing properties,
+--    which is not possible if cursors encapsulate an access to the underlying
+--    container.
+
+--    There are two new functions
+
+--      function Left  (Container : Set; Position : Cursor) return Set;
+--      function Right (Container : Set; Position : Cursor) return Set;
+
+--      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.
+
 private with Ada.Containers.Hash_Tables;
 private with Ada.Streams;
 
diff --git a/gcc/ada/a-cforma.ads b/gcc/ada/a-cforma.ads
index 25cb8a743e0..4debcd677ea 100644
--- a/gcc/ada/a-cforma.ads
+++ b/gcc/ada/a-cforma.ads
@@ -29,6 +29,31 @@
 -- <http://www.gnu.org/licenses/>.                                          --
 ------------------------------------------------------------------------------
 
+--  The specification of this package is derived from the specification
+--  of package Ada.Containers.Bounded_Ordered_Maps in the Ada 2012 RM.
+--  The changes are
+
+--    A parameter for the container is added to every function reading the
+--    content of a container: Key, Element, Next, Query_Element, Previous,
+--    Has_Element, Iterate, Reverse_Iterate. This change is
+--    motivated by the need to have cursors which are valid on different
+--    containers (typically a container C and its previous version C'Old) for
+--    expressing properties, which is not possible if cursors encapsulate an
+--    access to the underlying container. The operators "<" and ">" that could
+--    not be modified that way have been removed.
+
+--    There are two new functions
+
+--      function Left  (Container : Map; Position : Cursor) return Map;
+--      function Right (Container : Map; Position : Cursor) return Map;
+
+--      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.
+
 private with Ada.Containers.Red_Black_Trees;
 private with Ada.Streams;
 with Ada.Containers; use Ada.Containers;
diff --git a/gcc/ada/a-cforse.ads b/gcc/ada/a-cforse.ads
index 92c4e93497f..71eab933034 100644
--- a/gcc/ada/a-cforse.ads
+++ b/gcc/ada/a-cforse.ads
@@ -29,6 +29,31 @@
 -- <http://www.gnu.org/licenses/>.                                          --
 ------------------------------------------------------------------------------
 
+--  The specification of this package is derived from the specification
+--  of package Ada.Containers.Bounded_Ordered_Sets in the Ada 2012 RM.
+--  The changes are
+
+--    A parameter for the container is added to every function reading the
+--    content of a container: Key, Element, Next, Query_Element, Previous,
+--    Has_Element, Iterate, Reverse_Iterate. This change is
+--    motivated by the need to have cursors which are valid on different
+--    containers (typically a container C and its previous version C'Old) for
+--    expressing properties, which is not possible if cursors encapsulate an
+--    access to the underlying container. The operators "<" and ">" that could
+--    not be modified that way have been removed.
+
+--    There are two new functions
+
+--      function Left  (Container : Set; Position : Cursor) return Set;
+--      function Right (Container : Set; Position : Cursor) return Set;
+
+--      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.
+
 private with Ada.Containers.Red_Black_Trees;
 private with Ada.Streams;
 
diff --git a/gcc/ada/a-cofove.ads b/gcc/ada/a-cofove.ads
index d8e87f6695a..292e3ac0f88 100644
--- a/gcc/ada/a-cofove.ads
+++ b/gcc/ada/a-cofove.ads
@@ -29,6 +29,30 @@
 -- <http://www.gnu.org/licenses/>.                                          --
 ------------------------------------------------------------------------------
 
+--  The specification of this package is derived from the specification
+--  of package Ada.Containers.Bounded_Ordered_Maps in the Ada 2012 RM.
+--  The changes are
+
+--    A parameter for the container is added to every function reading the
+--    content of a container: Element, Next, Query_Element, Previous,
+--    Has_Element, Iterate, Reverse_Iterate. This change is
+--    motivated by the need to have cursors which are valid on different
+--    containers (typically a container C and its previous version C'Old) for
+--    expressing properties, which is not possible if cursors encapsulate an
+--    access to the underlying container.
+
+--    There are two new functions
+
+--      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.
+
 private with Ada.Streams;
 with Ada.Containers;
 use Ada.Containers;
diff --git a/gcc/ada/g-comlin.adb b/gcc/ada/g-comlin.adb
index e93042d9614..217328e5d14 100644
--- a/gcc/ada/g-comlin.adb
+++ b/gcc/ada/g-comlin.adb
@@ -673,15 +673,24 @@ package body GNAT.Command_Line is
                --  especially important when Concatenate is False, since
                --  otherwise the current argument first character is lost.
 
-               Set_Parameter
-                 (Parser.The_Switch,
-                  Arg_Num => Parser.Current_Argument,
-                  First   => Parser.Current_Index,
-                  Last    => Arg'Last,
-                  Extra   => Parser.Switch_Character);
-               Parser.Is_Switch (Parser.Current_Argument) := True;
-               Dummy := Goto_Next_Argument_In_Section (Parser);
-               return '*';
+               if Parser.Section (Parser.Current_Argument) = 0 then
+
+                  --  A section transition should not be returned to the user
+
+                  Dummy := Goto_Next_Argument_In_Section (Parser);
+                  goto Restart;
+
+               else
+                  Set_Parameter
+                    (Parser.The_Switch,
+                     Arg_Num => Parser.Current_Argument,
+                     First   => Parser.Current_Index,
+                     Last    => Arg'Last,
+                     Extra   => Parser.Switch_Character);
+                  Parser.Is_Switch (Parser.Current_Argument) := True;
+                  Dummy := Goto_Next_Argument_In_Section (Parser);
+                  return '*';
+               end if;
             end if;
 
             Set_Parameter
@@ -891,7 +900,14 @@ package body GNAT.Command_Line is
                Parser.Current_Section :=
                  Parser.Section (Parser.Current_Argument);
             end if;
-            return;
+
+            --  Until we have the start of another section
+
+            if Index = Parser.Section'Last
+               or else Parser.Section (Index + 1) /= 0
+            then
+               return;
+            end if;
          end if;
 
          Index := Index + 1;
@@ -1004,6 +1020,9 @@ package body GNAT.Command_Line is
                Delimiter_Found := True;
 
             elsif Parser.Section (Index) = 0 then
+
+               --  A previous section delimiter
+
                Delimiter_Found := False;
 
             elsif Delimiter_Found then
@@ -3186,14 +3205,14 @@ package body GNAT.Command_Line is
    procedure Getopt
      (Config   : Command_Line_Configuration;
       Callback : Switch_Handler := null;
-      Parser   : Opt_Parser := Command_Line_Parser)
+      Parser   : Opt_Parser     := Command_Line_Parser)
    is
       Getopt_Switches : String_Access;
-      C   : Character := ASCII.NUL;
+      C               : Character := ASCII.NUL;
 
-      Empty_Name : aliased constant String := "";
+      Empty_Name      : aliased constant String := "";
       Current_Section : Integer := -1;
-      Section_Name : not null access constant String := Empty_Name'Access;
+      Section_Name    : not null access constant String := Empty_Name'Access;
 
       procedure Simple_Callback
         (Simple_Switch : String;
@@ -3231,6 +3250,7 @@ package body GNAT.Command_Line is
                         Config.Switches (Index).Integer_Output.all :=
                           Integer'Value (Parameter);
                      end if;
+
                   exception
                      when Constraint_Error =>
                         raise Invalid_Parameter
diff --git a/gcc/ada/gnat_rm.texi b/gcc/ada/gnat_rm.texi
index 85fb454101f..e89468baf12 100644
--- a/gcc/ada/gnat_rm.texi
+++ b/gcc/ada/gnat_rm.texi
@@ -305,6 +305,12 @@ The GNAT Library
 * Ada.Characters.Wide_Latin_9 (a-cwila9.ads)::
 * Ada.Characters.Wide_Wide_Latin_1 (a-chzla1.ads)::
 * Ada.Characters.Wide_Wide_Latin_9 (a-chzla9.ads)::
+* Ada.Containers.Formal_Doubly_Linked_Lists (a-cfdlli.ads)::
+* Ada.Containers.Formal_Hashed_Maps (a-cfhama.ads)::
+* Ada.Containers.Formal_Hashed_Sets (a-cfhase.ads)::
+* Ada.Containers.Formal_Ordered_Maps (a-cforma.ads)::
+* Ada.Containers.Formal_Ordered_Sets (a-cforse.ads)::
+* Ada.Containers.Formal_Vectors (a-cofove.ads)::
 * Ada.Command_Line.Environment (a-colien.ads)::
 * Ada.Command_Line.Remove (a-colire.ads)::
 * Ada.Command_Line.Response_File (a-clrefi.ads)::
@@ -13871,6 +13877,12 @@ of GNAT, and will generate a warning message.
 * Ada.Characters.Wide_Latin_9 (a-cwila9.ads)::
 * Ada.Characters.Wide_Wide_Latin_1 (a-chzla1.ads)::
 * Ada.Characters.Wide_Wide_Latin_9 (a-chzla9.ads)::
+* Ada.Containers.Formal_Doubly_Linked_Lists (a-cfdlli.ads)::
+* Ada.Containers.Formal_Hashed_Maps (a-cfhama.ads)::
+* Ada.Containers.Formal_Hashed_Sets (a-cfhase.ads)::
+* Ada.Containers.Formal_Ordered_Maps (a-cforma.ads)::
+* Ada.Containers.Formal_Ordered_Sets (a-cforse.ads)::
+* Ada.Containers.Formal_Vectors (a-cofove.ads)::
 * Ada.Command_Line.Environment (a-colien.ads)::
 * Ada.Command_Line.Remove (a-colire.ads)::
 * Ada.Command_Line.Response_File (a-clrefi.ads)::
@@ -14073,6 +14085,66 @@ instead of @code{Character}.  The provision of such a package
 is specifically authorized by the Ada Reference Manual
 (RM A.3.3(27)).
 
+@node Ada.Containers.Formal_Doubly_Linked_Lists (a-cfdlli.ads)
+@section @code{Ada.Containers.Formal_Doubly_Linked_Lists} (@file{a-cfdlli.ads})
+@cindex @code{Ada.Containers.Formal_Doubly_Linked_Lists} (@file{a-cfdlli.ads})
+@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.
+
+@node Ada.Containers.Formal_Hashed_Maps (a-cfhama.ads)
+@section @code{Ada.Containers.Formal_Hashed_Maps} (@file{a-cfhama.ads})
+@cindex @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.
+
+@node Ada.Containers.Formal_Hashed_Sets (a-cfhase.ads)
+@section @code{Ada.Containers.Formal_Hashed_Sets} (@file{a-cfhase.ads})
+@cindex @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.
+
+@node Ada.Containers.Formal_Ordered_Maps (a-cforma.ads)
+@section @code{Ada.Containers.Formal_Ordered_Maps} (@file{a-cforma.ads})
+@cindex @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.
+
+@node Ada.Containers.Formal_Ordered_Sets (a-cforse.ads)
+@section @code{Ada.Containers.Formal_Ordered_Sets} (@file{a-cforse.ads})
+@cindex @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.
+
+@node Ada.Containers.Formal_Vectors (a-cofove.ads)
+@section @code{Ada.Containers.Formal_Vectors} (@file{a-cofove.ads})
+@cindex @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.
+
 @node Ada.Command_Line.Environment (a-colien.ads)
 @section @code{Ada.Command_Line.Environment} (@file{a-colien.ads})
 @cindex @code{Ada.Command_Line.Environment} (@file{a-colien.ads})