[multiple changes]

2011-08-02  Sergey Rybin  <rybin@adacore.com>

	* gnat_rm.texi: Ramification of pragma Eliminate documentation
	 - fix bugs in the description of Source_Trace;
	 - get rid of UNIT_NAME;

2011-08-02  Javier Miranda  <miranda@adacore.com>

	* exp_ch9.adb
	(Build_Dispatching_Requeue): Adding support for VM targets
	since we cannot directly reference the Tag entity.
	* exp_sel.adb (Build_K): Adding support for VM targets.
	(Build_S_Assignment): Adding support for VM targets.
	* exp_disp.adb
	(Default_Prim_Op_Position): In VM targets do not restrict availability
	of predefined interface primitives to compiling in Ada 2005 mode.
	(Is_Predefined_Interface_Primitive): In VM targets this service is not
	restricted to compiling in Ada 2005 mode.
	(Make_VM_TSD): Generate code that declares and initializes the OSD
	record. Needed to support dispatching calls through synchronized
	interfaces.
	* exp_ch3.adb
	(Make_Predefined_Primitive_Specs): Enable generation of predefined
	primitives associated with synchronized interfaces.
	(Make_Predefined_Primitive_Bodies): Enable generation of predefined
	primitives associated with synchronized interfaces.

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

	* par-ch11.adb (P_Handled_Sequence_Of_Statements): mark a sequence of
	statements hidden in SPARK if preceded by the HIDE directive
	(Parse_Exception_Handlers): mark each exception handler in a sequence of
	exception handlers as hidden in SPARK if preceded by the HIDE directive
	* par-ch6.adb (P_Subprogram): mark a subprogram body hidden in SPARK
	if starting with the HIDE directive
	* par-ch7.adb (P_Package): mark a package body hidden in SPARK if
	starting with the HIDE directive; mark the declarations in a private
	part as hidden in SPARK if the private part starts with the HIDE
	directive
	* restrict.adb, restrict.ads
	(Set_Hidden_Part_In_SPARK): record a range of slocs as hidden in SPARK
	(Is_In_Hidden_Part_In_SPARK): new function which returns whether its
	argument node belongs to a part which is hidden in SPARK
	(Check_SPARK_Restriction): do not issue violations on nodes in hidden
	parts in SPARK; protect the possibly costly call to
	Is_In_Hidden_Part_In_SPARK by a check that the SPARK restriction is on
	* scans.ads (Token_Type): new value Tok_SPARK_Hide in enumeration
	* scng.adb (Accumulate_Token_Checksum_GNAT_6_3,
	Accumulate_Token_Checksum_GNAT_5_03): add case for new token
	Tok_SPARK_Hide.
	(Scan): recognize special comment starting with '#' and followed by
	SPARK keyword "hide" as a HIDE directive.

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

	* types.ads, erroutc.ads: Minor reformatting.

2011-08-02  Vincent Celier  <celier@adacore.com>

	* link.c: Add response file support for cross platforms.

From-SVN: r177179

1 files changed, 42 insertions, 0 deletions

diff --git a/gcc/ada/restrict.adb b/gcc/ada/restrict.adb
index b37a593..e12dd63 100644
--- a/gcc/ada/restrict.adb
+++ b/gcc/ada/restrict.adb
@@ -119,6 +119,12 @@ package body Restrict is
    begin
       if Force or else Comes_From_Source (N) then
 
+         if Restriction_Check_Required (SPARK)
+           and then Is_In_Hidden_Part_In_SPARK (Sloc (N))
+         then
+            return;
+         end if;
+
          --  Since the call to Restriction_Msg from Check_Restriction may set
          --  Error_Msg_Sloc to the location of the pragma restriction, save and
          --  restore the previous value of the global variable around the call.
@@ -141,6 +147,12 @@ package body Restrict is
 
       if Comes_From_Source (N) then
 
+         if Restriction_Check_Required (SPARK)
+           and then Is_In_Hidden_Part_In_SPARK (Sloc (N))
+         then
+            return;
+         end if;
+
          --  Since the call to Restriction_Msg from Check_Restriction may set
          --  Error_Msg_Sloc to the location of the pragma restriction, save and
          --  restore the previous value of the global variable around the call.
@@ -548,6 +560,25 @@ package body Restrict is
       return Not_A_Restriction_Id;
    end Get_Restriction_Id;
 
+   --------------------------------
+   -- Is_In_Hidden_Part_In_SPARK --
+   --------------------------------
+
+   function Is_In_Hidden_Part_In_SPARK (Loc : Source_Ptr) return Boolean is
+   begin
+      --  Loop through table of hidden ranges
+
+      for J in SPARK_Hides.First .. SPARK_Hides.Last loop
+         if SPARK_Hides.Table (J).Start <= Loc
+           and then Loc <= SPARK_Hides.Table (J).Stop
+         then
+            return True;
+         end if;
+      end loop;
+
+      return False;
+   end Is_In_Hidden_Part_In_SPARK;
+
    -------------------------------
    -- No_Exception_Handlers_Set --
    -------------------------------
@@ -841,6 +872,17 @@ package body Restrict is
    end Same_Unit;
 
    ------------------------------
+   -- Set_Hidden_Part_In_SPARK --
+   ------------------------------
+
+   procedure Set_Hidden_Part_In_SPARK (Loc1, Loc2 : Source_Ptr) is
+   begin
+      SPARK_Hides.Increment_Last;
+      SPARK_Hides.Table (SPARK_Hides.Last).Start := Loc1;
+      SPARK_Hides.Table (SPARK_Hides.Last).Stop  := Loc2;
+   end Set_Hidden_Part_In_SPARK;
+
+   ------------------------------
    -- Set_Profile_Restrictions --
    ------------------------------