[multiple changes]

2013-10-14  Tristan Gingold  <gingold@adacore.com>

	* s-vmexta.ads: Add comments.

2013-10-14  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_ch6.adb (Analyze_Subprogram_Body_Contract): Add processing
	for pragma Refined_State.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Add processing
	for aspect Refined_Depends.
	* sem_prag.adb (Analyze_Contract_Cases_In_Decl_Part):
	Use Find_Related_Subprogram_Or_Body to find the related
	context. Use the current scope when determining whether to
	ensure proper visibility.
	(Analyze_Depends_In_Decl_Part):
	Add local variable Spec_Id. Update the comment on usage of
	Subp_Id. Use Find_Related_Subprogram_Or_Body to find the
	related context. Extract the corresponding spec of the body
	(if any). Use the current scope when determining when to
	ensure proper visibility.
	(Analyze_Global_In_Decl_Part):
	Add local variable Spec_Id. Update the comment on usage of
	Subp_Id. Use Find_Related_Subprogram_Or_Body to find the
	related context. Extract the corresponding spec of the body
	(if any). Use the current scope when determining when to
	ensure proper visibility.
	(Analyze_Global_Item): Use the
	entity of the subprogram spec when performing formal parameter
	checks. Perform state-related checks.
	(Analyze_Input_Output):
	Use Is_Attribute_Result to detect 'Result. Query the
	entity of a subprogram spec when verifying the prefix of
	'Result. Perform state-related checks.	(Analyze_Pragma):
	Merge the analysis of Refined_Depends and Refined_Global.
	(Analyze_Refined_Depends_In_Decl_Part): Provide implemenation.
	(Analyze_Refined_Global_In_Decl_Part): Move state-related checks
	to the body of Analyze_Global_In_Decl_Part. Rename local constant
	List to Items.	(Analyze_Refined_Pragma): Remove circuitry to
	find the proper context, use Find_Related_Subprogram_Or_Body
	instead.
	(Check_Function_Return): Query the entity of
	the subprogram spec when verifying the use of 'Result.
	(Check_In_Out_States, Check_Input_States, Check_Output_States):
	Avoid using Has_Null_Refinement to detect a state with
	a non-null refinement, use the Refinement_Constituents
	list instead.
	(Check_Matching_Constituent): Remove initialization code.
	(Check_Mode_Restriction_In_Function): Use the entity of the subprogram
	spec when verifying mode usage in functions.
	(Collect_Global_Items): New routine.
	(Collect_Subprogram_Inputs_Outputs): Add local
	variable Spec_Id. Add circuitry for bodies-as-specs. Use
	pragma Refined_Global when collecting for a body.
	(Create_Or_Modify_Clause): Use the location of the
	clause. Rename local variable Clause to New_Clause to avoid
	confusion and update all occurrences.  Use Is_Attribute_Result
	to detect 'Result.
	(Find_Related_Subprogram): Removed.
	(Find_Related_Subprogram_Or_Body): New routine.
	(Is_Part_Of): Move routine to top level.
	(Normalize_Clause): Update the
	comment on usage. The routine can now normalize a clause with
	multiple outputs by splitting it.
	(Collect_Global_Items):
	Rename local constant List to Items. Remove the check for
	a null list.
	(Requires_Profile_Installation): Removed.
	(Split_Multiple_Outputs): New routine.
	* sem_prag.ads: Update the comments on usage of various
	pragma-related analysis routines.
	* sem_util.adb (Contains_Refined_State): The routine can now
	process pragma [Refined_]Depends.
	(Has_Refined_State): Removed.
	(Has_State_In_Dependency): New routine.
	(Has_State_In_Global): New routine.
	(Is_Attribute_Result): New routine.
	* sem_util.ads (Is_Attribute_Result): New routine.

2013-10-14  Emmanuel Briot  <briot@adacore.com>

	* s-regpat.adb (Compile): Fix finalization of the automaton
	when its size was automatically computed to be exactly 1000 bytes.

2013-10-14  Ed Schonberg  <schonberg@adacore.com>

	* sem_ch3.adb (Complete_Private_Subtype): If the full view of
	the base type is constrained, the full view of the subtype is
	known to be constrained as well.

From-SVN: r203531

gcc/ada/ChangeLog

+2013-10-14  Tristan Gingold  <gingold@adacore.com>
+
+	* s-vmexta.ads: Add comments.
+
+2013-10-14  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* sem_ch6.adb (Analyze_Subprogram_Body_Contract): Add processing
+	for pragma Refined_State.
+	* sem_ch13.adb (Analyze_Aspect_Specifications): Add processing
+	for aspect Refined_Depends.
+	* sem_prag.adb (Analyze_Contract_Cases_In_Decl_Part):
+	Use Find_Related_Subprogram_Or_Body to find the related
+	context. Use the current scope when determining whether to
+	ensure proper visibility.
+	(Analyze_Depends_In_Decl_Part):
+	Add local variable Spec_Id. Update the comment on usage of
+	Subp_Id. Use Find_Related_Subprogram_Or_Body to find the
+	related context. Extract the corresponding spec of the body
+	(if any). Use the current scope when determining when to
+	ensure proper visibility.
+	(Analyze_Global_In_Decl_Part):
+	Add local variable Spec_Id. Update the comment on usage of
+	Subp_Id. Use Find_Related_Subprogram_Or_Body to find the
+	related context. Extract the corresponding spec of the body
+	(if any). Use the current scope when determining when to
+	ensure proper visibility.
+	(Analyze_Global_Item): Use the
+	entity of the subprogram spec when performing formal parameter
+	checks. Perform state-related checks.
+	(Analyze_Input_Output):
+	Use Is_Attribute_Result to detect 'Result. Query the
+	entity of a subprogram spec when verifying the prefix of
+	'Result. Perform state-related checks.	(Analyze_Pragma):
+	Merge the analysis of Refined_Depends and Refined_Global.
+	(Analyze_Refined_Depends_In_Decl_Part): Provide implemenation.
+	(Analyze_Refined_Global_In_Decl_Part): Move state-related checks
+	to the body of Analyze_Global_In_Decl_Part. Rename local constant
+	List to Items.	(Analyze_Refined_Pragma): Remove circuitry to
+	find the proper context, use Find_Related_Subprogram_Or_Body
+	instead.
+	(Check_Function_Return): Query the entity of
+	the subprogram spec when verifying the use of 'Result.
+	(Check_In_Out_States, Check_Input_States, Check_Output_States):
+	Avoid using Has_Null_Refinement to detect a state with
+	a non-null refinement, use the Refinement_Constituents
+	list instead.
+	(Check_Matching_Constituent): Remove initialization code.
+	(Check_Mode_Restriction_In_Function): Use the entity of the subprogram
+	spec when verifying mode usage in functions.
+	(Collect_Global_Items): New routine.
+	(Collect_Subprogram_Inputs_Outputs): Add local
+	variable Spec_Id. Add circuitry for bodies-as-specs. Use
+	pragma Refined_Global when collecting for a body.
+	(Create_Or_Modify_Clause): Use the location of the
+	clause. Rename local variable Clause to New_Clause to avoid
+	confusion and update all occurrences.  Use Is_Attribute_Result
+	to detect 'Result.
+	(Find_Related_Subprogram): Removed.
+	(Find_Related_Subprogram_Or_Body): New routine.
+	(Is_Part_Of): Move routine to top level.
+	(Normalize_Clause): Update the
+	comment on usage. The routine can now normalize a clause with
+	multiple outputs by splitting it.
+	(Collect_Global_Items):
+	Rename local constant List to Items. Remove the check for
+	a null list.
+	(Requires_Profile_Installation): Removed.
+	(Split_Multiple_Outputs): New routine.
+	* sem_prag.ads: Update the comments on usage of various
+	pragma-related analysis routines.
+	* sem_util.adb (Contains_Refined_State): The routine can now
+	process pragma [Refined_]Depends.
+	(Has_Refined_State): Removed.
+	(Has_State_In_Dependency): New routine.
+	(Has_State_In_Global): New routine.
+	(Is_Attribute_Result): New routine.
+	* sem_util.ads (Is_Attribute_Result): New routine.
+
+2013-10-14  Emmanuel Briot  <briot@adacore.com>
+
+	* s-regpat.adb (Compile): Fix finalization of the automaton
+	when its size was automatically computed to be exactly 1000 bytes.
+
+2013-10-14  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_ch3.adb (Complete_Private_Subtype): If the full view of
+	the base type is constrained, the full view of the subtype is
+	known to be constrained as well.
+
 2013-10-14  Vincent Celier  <celier@adacore.com>
 
 	* projects.texi: Add documentation for new attributes of package

gcc/ada/s-regpat.adb

@@ -7,7 +7,7 @@
 --                                 B o d y                                  --
 --                                                                          --
 --               Copyright (C) 1986 by University of Toronto.               --
---                      Copyright (C) 1999-2011, AdaCore                    --
+--                      Copyright (C) 1999-2013, AdaCore                    --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -921,7 +921,7 @@ package body System.Regpat is
 
          Link_Tail (IP, Ender);
 
-         if Have_Branch and then Emit_Ptr <= PM.Size then
+         if Have_Branch and then Emit_Ptr <= PM.Size + 1 then
 
             --  Hook the tails of the branches to the closing node
 

gcc/ada/s-vmexta.ads

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1997-2009, Free Software Foundation, Inc.         --
+--          Copyright (C) 1997-2013, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -29,7 +29,7 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
---  This package is usually used only on Alpha/VMS systems in the case
+--  This package is usually used only on OpenVMS systems in the case
 --  where there is at least one Import/Export exception present.
 
 with System.Standard_Library;
@@ -44,16 +44,23 @@ package System.VMS_Exception_Table is
    --  Register an exception in the hash table mapping with a VMS
    --  condition code.
 
+   --  The table is used by exception code (the personnality routine) to
+   --  detect wether a VMS exception (aka condition) is known by the Ada code.
+   --  In that case, the identity of the imported or exported exception is
+   --  used to create the occurrence.
+
    --  LOTS more comments needed here regarding the entire scheme ???
 
 private
 
+   --  The following functions are directly called (without import/export) in
+   --  init.c by __gnat_handle_vms_condition.
+
    function Base_Code_In (Code : SSL.Exception_Code) return SSL.Exception_Code;
    --  Value of Code with the severity bits masked off
 
    function Coded_Exception (X : SSL.Exception_Code)
      return SSL.Exception_Data_Ptr;
    --  Given a VMS condition, find and return it's allocated Ada exception
-   --  (called only from init.c).
 
 end System.VMS_Exception_Table;

gcc/ada/sem_ch13.adb

@@ -1998,10 +1998,21 @@ package body Sem_Ch13 is
 
                --  Refined_Depends
 
-               --  ??? To be implemented
+               --  Aspect Refined_Depends must be delayed because it can
+               --  mention state refinements introduced by aspect Refined_State
+               --  and further classified by aspect Refined_Global. Since both
+               --  those aspects are delayed, so is Refined_Depends.
 
                when Aspect_Refined_Depends =>
-                  null;
+                  Make_Aitem_Pragma
+                    (Pragma_Argument_Associations => New_List (
+                       Make_Pragma_Argument_Association (Loc,
+                         Expression => Relocate_Node (Expr))),
+                     Pragma_Name                  => Name_Refined_Depends);
+
+                  Decorate_Delayed_Aspect_And_Pragma (Aspect, Aitem);
+                  Insert_Delayed_Pragma (Aitem);
+                  goto Continue;
 
                --  Refined_Global
 

gcc/ada/sem_ch3.adb

@@ -10393,6 +10393,14 @@ package body Sem_Ch3 is
             Set_First_Entity (Full, First_Entity (Full_Base));
             Set_Last_Entity  (Full, Last_Entity (Full_Base));
 
+            --  If the underlying base type is constrained, we know that the
+            --  full view of the subtype is constrained as well (the converse
+            --  is not necessarily true).
+
+            if Is_Constrained (Full_Base) then
+               Set_Is_Constrained (Full);
+            end if;
+
          when others =>
             Copy_Node (Full_Base, Full);
 

gcc/ada/sem_ch6.adb

@@ -2029,6 +2029,18 @@ package body Sem_Ch6 is
 
       if Present (Ref_Depends) then
          Analyze_Refined_Depends_In_Decl_Part (Ref_Depends);
+
+      --  When the corresponding Depends aspect/pragma references a state with
+      --  visible refinement, the body requires Refined_Depends.
+
+      elsif Present (Spec_Id) then
+         Prag := Get_Pragma (Spec_Id, Pragma_Depends);
+
+         if Present (Prag) and then Contains_Refined_State (Prag) then
+            Error_Msg_NE
+              ("body of subprogram & requires dependance refinement",
+               Body_Decl, Spec_Id);
+         end if;
       end if;
    end Analyze_Subprogram_Body_Contract;
 

gcc/ada/sem_prag.ads

@@ -57,10 +57,12 @@ package Sem_Prag is
    --  Perform full analysis and expansion of delayed pragma Contract_Cases
 
    procedure Analyze_Depends_In_Decl_Part (N : Node_Id);
-   --  Perform full analysis of delayed pragma Depends
+   --  Perform full analysis of delayed pragma Depends. This routine is also
+   --  capable of performing basic analysis of pragma Refined_Depends.
 
    procedure Analyze_Global_In_Decl_Part (N : Node_Id);
-   --  Perform full analysis of delayed pragma Global
+   --  Perform full analysis of delayed pragma Global. This routine is also
+   --  capable of performing basic analysis of pragma Refind_Global.
 
    procedure Analyze_Initializes_In_Decl_Part (N : Node_Id);
    --  Perform full analysis of delayed pragma Initializes
@@ -75,10 +77,14 @@ package Sem_Prag is
    --  of Default and Per-Object Expressions in Sem).
 
    procedure Analyze_Refined_Depends_In_Decl_Part (N : Node_Id);
-   --  Preform full analysis of delayed pragma Refined_Depends
+   --  Preform full analysis of delayed pragma Refined_Depends. This routine
+   --  uses Analyze_Depends_In_Decl_Part as a starting point, then performs
+   --  various consistency checks between Depends and Refined_Depends.
 
    procedure Analyze_Refined_Global_In_Decl_Part (N : Node_Id);
-   --  Perform full analysis of delayed pragma Refined_Global
+   --  Perform full analysis of delayed pragma Refined_Global. This routine
+   --  uses Analyze_Global_In_Decl_Part as a starting point, then performs
+   --  various consistency checks between Global and Refined_Global.
 
    procedure Analyze_Refined_State_In_Decl_Part (N : Node_Id);
    --  Perform full analysis of delayed pragma Refined_State

gcc/ada/sem_util.adb

@@ -3242,44 +3242,79 @@ package body Sem_Util is
    ----------------------------
 
    function Contains_Refined_State (Prag : Node_Id) return Boolean is
-      function Has_Refined_State (List : Node_Id) return Boolean;
+      function Has_State_In_Dependency (List : Node_Id) return Boolean;
+      --  Determine whether a dependency list mentions a state with a visible
+      --  refinement.
+
+      function Has_State_In_Global (List : Node_Id) return Boolean;
       --  Determine whether a global list mentions a state with a visible
       --  refinement.
 
-      -----------------------
-      -- Has_Refined_State --
-      -----------------------
+      function Is_Refined_State (Item : Node_Id) return Boolean;
+      --  Determine whether Item is a reference to an abstract state with a
+      --  visible refinement.
 
-      function Has_Refined_State (List : Node_Id) return Boolean is
-         function Is_Refined_State (Item : Node_Id) return Boolean;
-         --  Determine whether Item is a reference to an abstract state with a
-         --  visible refinement.
+      -----------------------------
+      -- Has_State_In_Dependency --
+      -----------------------------
 
-         ----------------------
-         -- Is_Refined_State --
-         ----------------------
+      function Has_State_In_Dependency (List : Node_Id) return Boolean is
+         Clause : Node_Id;
+         Output : Node_Id;
 
-         function Is_Refined_State (Item : Node_Id) return Boolean is
-            Item_Id : Entity_Id;
+      begin
+         --  A null dependency list does not mention any states
 
-         begin
-            if Nkind (Item) = N_Null then
-               return False;
+         if Nkind (List) = N_Null then
+            return False;
 
-            else
-               Item_Id := Entity_Of (Item);
+         --  Dependency clauses appear as component associations of an
+         --  aggregate.
 
-               return
-                 Ekind (Item_Id) = E_Abstract_State
-                   and then Present (Refinement_Constituents (Item_Id));
-            end if;
-         end Is_Refined_State;
+         elsif Nkind (List) = N_Aggregate
+           and then Present (Component_Associations (List))
+         then
+            Clause := First (Component_Associations (List));
+            while Present (Clause) loop
 
-         --  Local variables
+               --  Inspect the outputs of a dependency clause
 
-         Item : Node_Id;
+               Output := First (Choices (Clause));
+               while Present (Output) loop
+                  if Is_Refined_State (Output) then
+                     return True;
+                  end if;
+
+                  Next (Output);
+               end loop;
 
-      --  Start of processing for Has_Refined_State
+               --  Inspect the outputs of a dependency clause
+
+               if Is_Refined_State (Expression (Clause)) then
+                  return True;
+               end if;
+
+               Next (Clause);
+            end loop;
+
+            --  If we get here, then none of the dependency clauses mention a
+            --  state with visible refinement.
+
+            return False;
+
+         --  An illegal pragma managed to sneak in
+
+         else
+            raise Program_Error;
+         end if;
+      end Has_State_In_Dependency;
+
+      -------------------------
+      -- Has_State_In_Global --
+      -------------------------
+
+      function Has_State_In_Global (List : Node_Id) return Boolean is
+         Item : Node_Id;
 
       begin
          --  A null global list does not mention any states
@@ -3287,14 +3322,6 @@ package body Sem_Util is
          if Nkind (List) = N_Null then
             return False;
 
-         --  Single global item declaration
-
-         elsif Nkind_In (List, N_Expanded_Name,
-                               N_Identifier,
-                               N_Selected_Component)
-         then
-            return Is_Refined_State (List);
-
          --  Simple global list or moded global list declaration
 
          elsif Nkind (List) = N_Aggregate then
@@ -3319,7 +3346,7 @@ package body Sem_Util is
             else
                Item := First (Component_Associations (List));
                while Present (Item) loop
-                  if Has_Refined_State (Expression (Item)) then
+                  if Has_State_In_Global (Expression (Item)) then
                      return True;
                   end if;
 
@@ -3332,12 +3359,68 @@ package body Sem_Util is
 
             return False;
 
-         --  Something went horribly wrong, we have a malformed tree
+         --  Single global item declaration
+
+         elsif Is_Entity_Name (List) then
+            return Is_Refined_State (List);
+
+         --  An illegal pragma managed to sneak in
 
          else
             raise Program_Error;
          end if;
-      end Has_Refined_State;
+      end Has_State_In_Global;
+
+      ----------------------
+      -- Is_Refined_State --
+      ----------------------
+
+      function Is_Refined_State (Item : Node_Id) return Boolean is
+         Elmt    : Node_Id;
+         Item_Id : Entity_Id;
+
+      begin
+         if Nkind (Item) = N_Null then
+            return False;
+
+         --  States cannot be subject to attribute 'Result. This case arises
+         --  in dependency relations.
+
+         elsif Nkind (Item) = N_Attribute_Reference
+           and then Attribute_Name (Item) = Name_Result
+         then
+            return False;
+
+         --  Multiple items appear as an aggregate. This case arises in
+         --  dependency relations.
+
+         elsif Nkind (Item) = N_Aggregate
+           and then Present (Expressions (Item))
+         then
+            Elmt := First (Expressions (Item));
+            while Present (Elmt) loop
+               if Is_Refined_State (Elmt) then
+                  return True;
+               end if;
+
+               Next (Elmt);
+            end loop;
+
+            --  If we get here, then none of the inputs or outputs reference a
+            --  state with visible refinement.
+
+            return False;
+
+         --  Single item
+
+         else
+            Item_Id := Entity_Of (Item);
+
+            return
+              Ekind (Item_Id) = E_Abstract_State
+                and then Present (Refinement_Constituents (Item_Id));
+         end if;
+      end Is_Refined_State;
 
       --  Local variables
 
@@ -3348,13 +3431,11 @@ package body Sem_Util is
    --  Start of processing for Contains_Refined_State
 
    begin
-      --  ??? To be implemented
-
       if Nam = Name_Depends then
-         return False;
+         return Has_State_In_Dependency (Arg);
 
       else pragma Assert (Nam = Name_Global);
-         return Has_Refined_State (Arg);
+         return Has_State_In_Global (Arg);
       end if;
    end Contains_Refined_State;
 
@@ -8188,6 +8269,17 @@ package body Sem_Util is
       end if;
    end Is_Atomic_Object;
 
+   -------------------------
+   -- Is_Attribute_Result --
+   -------------------------
+
+   function Is_Attribute_Result (N : Node_Id) return Boolean is
+   begin
+      return
+         Nkind (N) = N_Attribute_Reference
+           and then Attribute_Name (N) = Name_Result;
+   end Is_Attribute_Result;
+
    ------------------------------------
    -- Is_Body_Or_Package_Declaration --
    ------------------------------------

gcc/ada/sem_util.ads

@@ -902,6 +902,9 @@ package Sem_Util is
    --  Determines if the given node denotes an atomic object in the sense of
    --  the legality checks described in RM C.6(12).
 
+   function Is_Attribute_Result (N : Node_Id) return Boolean;
+   --  Determine whether node N denotes attribute 'Result
+
    function Is_Body_Or_Package_Declaration (N : Node_Id) return Boolean;
    --  Determine whether node N denotes a body or a package declaration