2014-02-19 Matthew Heaney <heaney@adacore.com>

	* a-chtgop.ads (Checked_Index): New operation.
	(Next): Changed mode of hash table.
	* a-chtgop.adb (Adjust, Delete_Node_Sans_Free): Detect tampering
	(Generic_Read, Reserve_Capacity): Ditto.
	(Generic_Equal): Detect tampering.
	(Next): Changed mode of hash table, detect tampering.
	* a-chtgke.ads (Checked_Index, Checked_Equivalent_Keys): New
	operation.
	(Find): Changed mode of hash table.
	* a-chtgke.adb (Checked_Equivalent_Keys): New operation
	(Delete_Key_Sans_Free, Generic_Conditional_Insert): Detect
	tampering.
	(Find): Changed mode of hash table, check for tampering.
	(Generic_Replace_Element): Check for tampering.
	* a-chtgbk.ads (Checked_Index, Checked_Equivalent_Keys): New operation.
	* a-chtgbk.adb (Checked_Index, Checked_Equivalent_Keys): New
	operation (Delete_Key_Sans_Free, Generic_Conditional_Insert):
	Detect tampering.
	(Find, Generic_Replace_Element): Check for tampering.
	* a-chtgbo.ads (Checked_Index): New operation.
	* a-chtgbo.adb (Checked_Index): New operation
	(Delete_Node_Sans_Free, Generic_Equal): Detect tampering.
	(Generic_Read, Next): Ditto.
	* a-cohase.adb, a-cihase.adb (Is_In): Changed mode of hash
	table (Difference, Intersection): Use variable view of
	source, detect tampering (Find, Is_Subset, Overlap): Use
	variable view of container (Symmetric_Difference, Union):
	Detect tampering (Vet): Use Checked_Index to detect tampering
	(Constant_Reference, Element, Find): Use variable view of
	container.
	(Update_Element_Preserving_Key): Detect tampering.
	* a-cbhase.adb (Difference, Find, Is_In): Use variable view
	of container.
	(Is_Subset): Ditto.
	(Equivalent_Sets, Overlap): Use Node's Next component.
	(Vet): Use Checked_Index to detect tampering.
	(Constant_Reference, Element, Find): Use variable view of container.
	(Update_Element_Preserving_Key): Detect tampering.
	* a-cohama.adb, a-cihama.adb, a-cbhama.adb (Constant_Reference,
	Element, Find): Use variable view of container.
	(Reference): Rename hash table component.
	(Vet): Use Checked_Index to detect tampering.

2014-02-19  Arnaud Charlet  <charlet@adacore.com>

	* adabkend.adb (Scan_Compiler_Arguments): Add missing handling
	of -nostdinc.

2014-02-19  Thomas Quinot  <quinot@adacore.com>

	* tbuild.adb (New_Occurrence_Of, New_Rerefence_To): Guard
	against calls without Def_Id.

2014-02-19  Claire Dross  <dross@adacore.com>

	* a-cfdlli.ads, a-cfhase.ads, a-cforma.ads, a-cfhama.ads, a-cforse.ads,
	a-cofove.ads: Add global annotations to subprograms.

2014-02-19  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_prag.adb (Analyze_Initial_Condition_In_Decl_Part): Remove
	constants Errors, Pack_Id and Pack_Init. Remove variable Vars.
	Initial_Condition no longer requires the presence of pragma
	Initialized. Do not try to diagnose whether all variables mentioned in
	pragma Initializes also appear in Initial_Condition.
	(Collect_Variables): Removed.
	(Match_Variable): Removed.
	(Match_Variables): Removed.
	(Report_Unused_Variables): Removed.

2014-02-19  Thomas Quinot  <quinot@adacore.com>

	* gnat_rm.texi (pragma Stream_Convert): Minor rewording.



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

1 files changed, 82 insertions, 41 deletions

diff --git a/gcc/ada/a-cforma.ads b/gcc/ada/a-cforma.ads
index 08dabf5541f..f927cf86da3 100644
--- a/gcc/ada/a-cforma.ads
+++ b/gcc/ada/a-cforma.ads
@@ -68,7 +68,8 @@ package Ada.Containers.Formal_Ordered_Maps is
    pragma Annotate (GNATprove, External_Axiomatization);
    pragma Pure;
 
-   function Equivalent_Keys (Left, Right : Key_Type) return Boolean;
+   function Equivalent_Keys (Left, Right : Key_Type) return Boolean with
+     Global => null;
 
    type Map (Capacity : Count_Type) is private with
      Iterable => (First       => First,
@@ -84,38 +85,48 @@ package Ada.Containers.Formal_Ordered_Maps is
 
    No_Element : constant Cursor;
 
-   function "=" (Left, Right : Map) return Boolean;
+   function "=" (Left, Right : Map) return Boolean with
+     Global => null;
 
-   function Length (Container : Map) return Count_Type;
+   function Length (Container : Map) return Count_Type with
+     Global => null;
 
-   function Is_Empty (Container : Map) return Boolean;
+   function Is_Empty (Container : Map) return Boolean with
+     Global => null;
 
-   procedure Clear (Container : in out Map);
+   procedure Clear (Container : in out Map) with
+     Global => null;
 
    procedure Assign (Target : in out Map; Source : Map) with
-     Pre => Target.Capacity >= Length (Source);
+     Global => null,
+     Pre    => Target.Capacity >= Length (Source);
 
    function Copy (Source : Map; Capacity : Count_Type := 0) return Map with
-     Pre => Capacity = 0 or else Capacity >= Source.Capacity;
+     Global => null,
+     Pre    => Capacity = 0 or else Capacity >= Source.Capacity;
 
    function Key (Container : Map; Position : Cursor) return Key_Type with
-     Pre => Has_Element (Container, Position);
+     Global => null,
+     Pre    => Has_Element (Container, Position);
 
    function Element
      (Container : Map;
       Position  : Cursor) return Element_Type
    with
-     Pre => Has_Element (Container, Position);
+     Global => null,
+     Pre    => Has_Element (Container, Position);
 
    procedure Replace_Element
      (Container : in out Map;
       Position  : Cursor;
       New_Item  : Element_Type)
    with
-     Pre => Has_Element (Container, Position);
+     Global => null,
+     Pre    => Has_Element (Container, Position);
 
    procedure Move (Target : in out Map; Source : in out Map) with
-     Pre => Target.Capacity >= Length (Source);
+     Global => null,
+     Pre    => Target.Capacity >= Length (Source);
 
    procedure Insert
      (Container : in out Map;
@@ -124,92 +135,121 @@ package Ada.Containers.Formal_Ordered_Maps is
       Position  : out Cursor;
       Inserted  : out Boolean)
    with
-     Pre => Length (Container) < Container.Capacity;
+     Global => null,
+     Pre    => Length (Container) < Container.Capacity;
 
    procedure Insert
      (Container : in out Map;
       Key       : Key_Type;
       New_Item  : Element_Type)
    with
-     Pre => Length (Container) < Container.Capacity
-              and then (not Contains (Container, Key));
+     Global => null,
+     Pre    => Length (Container) < Container.Capacity
+                 and then (not Contains (Container, Key));
 
    procedure Include
      (Container : in out Map;
       Key       : Key_Type;
       New_Item  : Element_Type)
    with
-     Pre => Length (Container) < Container.Capacity;
+     Global => null,
+     Pre    => Length (Container) < Container.Capacity;
 
    procedure Replace
      (Container : in out Map;
       Key       : Key_Type;
       New_Item  : Element_Type)
    with
-     Pre => Contains (Container, Key);
+     Global => null,
+     Pre    => Contains (Container, Key);
 
-   procedure Exclude (Container : in out Map; Key : Key_Type);
+   procedure Exclude (Container : in out Map; Key : Key_Type) with
+     Global => null;
 
    procedure Delete (Container : in out Map; Key : Key_Type) with
-     Pre => Contains (Container, Key);
+     Global => null,
+     Pre    => Contains (Container, Key);
 
    procedure Delete (Container : in out Map; Position : in out Cursor) with
-     Pre => Has_Element (Container, Position);
+     Global => null,
+     Pre    => Has_Element (Container, Position);
 
-   procedure Delete_First (Container : in out Map);
+   procedure Delete_First (Container : in out Map) with
+     Global => null;
 
-   procedure Delete_Last (Container : in out Map);
+   procedure Delete_Last (Container : in out Map) with
+     Global => null;
 
-   function First (Container : Map) return Cursor;
+   function First (Container : Map) return Cursor with
+     Global => null;
 
    function First_Element (Container : Map) return Element_Type with
-     Pre => not Is_Empty (Container);
+     Global => null,
+     Pre    => not Is_Empty (Container);
 
    function First_Key (Container : Map) return Key_Type with
-     Pre => not Is_Empty (Container);
+     Global => null,
+     Pre    => not Is_Empty (Container);
 
-   function Last (Container : Map) return Cursor;
+   function Last (Container : Map) return Cursor with
+     Global => null;
 
    function Last_Element (Container : Map) return Element_Type with
-     Pre => not Is_Empty (Container);
+     Global => null,
+     Pre    => not Is_Empty (Container);
 
    function Last_Key (Container : Map) return Key_Type with
-     Pre => not Is_Empty (Container);
+     Global => null,
+     Pre    => not Is_Empty (Container);
 
    function Next (Container : Map; Position : Cursor) return Cursor with
-     Pre => Has_Element (Container, Position) or else Position = No_Element;
+     Global => null,
+     Pre    => Has_Element (Container, Position) or else Position = No_Element;
 
    procedure Next (Container : Map; Position : in out Cursor) with
-     Pre => Has_Element (Container, Position) or else Position = No_Element;
+     Global => null,
+     Pre    => Has_Element (Container, Position) or else Position = No_Element;
 
    function Previous (Container : Map; Position : Cursor) return Cursor with
-     Pre => Has_Element (Container, Position) or else Position = No_Element;
+     Global => null,
+     Pre    => Has_Element (Container, Position) or else Position = No_Element;
 
    procedure Previous (Container : Map; Position : in out Cursor) with
-     Pre => Has_Element (Container, Position) or else Position = No_Element;
+     Global => null,
+     Pre    => Has_Element (Container, Position) or else Position = No_Element;
 
-   function Find (Container : Map; Key : Key_Type) return Cursor;
+   function Find (Container : Map; Key : Key_Type) return Cursor with
+     Global => null;
 
    function Element (Container : Map; Key : Key_Type) return Element_Type with
-     Pre => Contains (Container, Key);
+     Global => null,
+     Pre    => Contains (Container, Key);
 
-   function Floor (Container : Map; Key : Key_Type) return Cursor;
+   function Floor (Container : Map; Key : Key_Type) return Cursor with
+     Global => null;
 
-   function Ceiling (Container : Map; Key : Key_Type) return Cursor;
+   function Ceiling (Container : Map; Key : Key_Type) return Cursor with
+     Global => null;
 
-   function Contains (Container : Map; Key : Key_Type) return Boolean;
+   function Contains (Container : Map; Key : Key_Type) return Boolean with
+     Global => null;
 
-   function Has_Element (Container : Map; Position : Cursor) return Boolean;
+   function Has_Element (Container : Map; Position : Cursor) return Boolean
+   with
+     Global => null;
 
-   function Strict_Equal (Left, Right : Map) return Boolean;
+   function Strict_Equal (Left, Right : Map) return Boolean with
+     Global => null;
    --  Strict_Equal returns True if the containers are physically equal, i.e.
    --  they are structurally equal (function "=" returns True) and that they
    --  have the same set of cursors.
 
    function Left  (Container : Map; Position : Cursor) return Map with
-     Pre => Has_Element (Container, Position) or else Position = No_Element;
+     Global => null,
+     Pre    => Has_Element (Container, Position) or else Position = No_Element;
    function Right (Container : Map; Position : Cursor) return Map with
-     Pre => Has_Element (Container, Position) or else Position = No_Element;
+     Global => null,
+     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
@@ -217,7 +257,8 @@ package Ada.Containers.Formal_Ordered_Maps is
    --  iterate over containers. Left returns the part of the container already
    --  scanned and Right the part not scanned yet.
 
-   function Overlap (Left, Right : Map) return Boolean;
+   function Overlap (Left, Right : Map) return Boolean with
+     Global => null;
    --  Overlap returns True if the containers have common keys
 private