From 4a3ade652da8276a8249df55677f56eda9246b6f Mon Sep 17 00:00:00 2001 From: charlet Date: Tue, 2 Aug 2011 09:46:08 +0000 Subject: [PATCH] 2011-08-02 Claire Dross * 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 * gnat_rm.texi: Document formal containers. 2011-08-02 Emmanuel Briot * 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 --- gcc/ada/ChangeLog | 14 ++++++++++ gcc/ada/a-cfdlli.ads | 24 ++++++++++++++++++ gcc/ada/a-cfhama.ads | 24 ++++++++++++++++++ gcc/ada/a-cfhase.ads | 24 ++++++++++++++++++ gcc/ada/a-cforma.ads | 25 ++++++++++++++++++ gcc/ada/a-cforse.ads | 25 ++++++++++++++++++ gcc/ada/a-cofove.ads | 24 ++++++++++++++++++ gcc/ada/g-comlin.adb | 48 +++++++++++++++++++++++++---------- gcc/ada/gnat_rm.texi | 72 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 9 files changed, 266 insertions(+), 14 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index c6a2ff8..66995e3 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,17 @@ +2011-08-02 Claire Dross + + * 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 + + * gnat_rm.texi: Document formal containers. + +2011-08-02 Emmanuel Briot + + * g-comlin.adb (Goto_Section, Getopt): fix handling of "*" when there + are empty sections. + 2011-08-02 Robert Dewar * 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 af64ea3..526410c 100644 --- a/gcc/ada/a-cfdlli.ads +++ b/gcc/ada/a-cfdlli.ads @@ -29,6 +29,30 @@ -- . -- ------------------------------------------------------------------------------ +-- 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 03b6d36..f11f5da 100644 --- a/gcc/ada/a-cfhama.ads +++ b/gcc/ada/a-cfhama.ads @@ -29,6 +29,30 @@ -- . -- ------------------------------------------------------------------------------ +-- 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 2a6a613..33c10c6 100644 --- a/gcc/ada/a-cfhase.ads +++ b/gcc/ada/a-cfhase.ads @@ -29,6 +29,30 @@ -- . -- ------------------------------------------------------------------------------ +-- 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 25cb8a7..4debcd6 100644 --- a/gcc/ada/a-cforma.ads +++ b/gcc/ada/a-cforma.ads @@ -29,6 +29,31 @@ -- . -- ------------------------------------------------------------------------------ +-- 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 92c4e93..71eab933 100644 --- a/gcc/ada/a-cforse.ads +++ b/gcc/ada/a-cforse.ads @@ -29,6 +29,31 @@ -- . -- ------------------------------------------------------------------------------ +-- 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 d8e87f6..292e3ac 100644 --- a/gcc/ada/a-cofove.ads +++ b/gcc/ada/a-cofove.ads @@ -29,6 +29,30 @@ -- . -- ------------------------------------------------------------------------------ +-- 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 e93042d..217328e 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 85fb454..e89468b 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}) -- 2.7.4