From 300b98bbaac6c3d4762715205895161fd420ff9f Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Tue, 2 Aug 2011 11:46:08 +0200 Subject: [PATCH] [multiple changes] 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. From-SVN: r177111 --- 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 c6a2ff86f88..66995e3a36f 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 af64ea35f8b..526410c3b79 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 03b6d36789d..f11f5dac723 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 2a6a613b3da..33c10c693f9 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 25cb8a743e0..4debcd677ea 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 92c4e93497f..71eab933034 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 d8e87f6695a..292e3ac0f88 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 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}) -- 2.30.2