+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
-- <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;
-- <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;
-- <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;
-- <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;
-- <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;
-- <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;
-- 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
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;
Delimiter_Found := True;
elsif Parser.Section (Index) = 0 then
+
+ -- A previous section delimiter
+
Delimiter_Found := False;
elsif Delimiter_Found then
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;
Config.Switches (Index).Integer_Output.all :=
Integer'Value (Parameter);
end if;
+
exception
when Constraint_Error =>
raise Invalid_Parameter
* 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)::
* 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)::
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})
projects / gcc.git / commitdiff