[multiple changes]

2013-10-17  Robert Dewar  <dewar@adacore.com>

	* sem_prag.adb (Record_Possible_Body_Reference): Fix test for
	being in body.
	(Add_Constituent): Merged into Check_Refined_Global_Item.
	(Check_Matching_Constituent): A constituent that has the proper Part_Of
	option and comes from a private child or a sibling is now collected.
	(Check_Matching_Modes): Merged into Check_Refined_Global_Item.
	(Check_Refined_Global_Item): Code cleanup.
	(Collect_Constituent): New routine.
	(Inconsistent_Mode_Error): Moved out from Check_Matching_Modes.

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

	* freeze.adb (Check_Current_Instance, Process): Add RM reference
	and mention immutably limited types, when the current instance
	is illegal in Ada 2012.

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

	* sem_warn.adb (Check_Unused_Withs): If the main unit is a
	subunit, apply the check to the units mentioned in its context
	only. This provides additional warnings on with_clauses that
	are superfluous.

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

	* sem_ch3.adb (Analyze_Declarations): Emit an
	error message concerning state refinement when the spec defines at
	least one non-null abstract state and the body's SPARK mode is On.
	(Requires_State_Refinement): New routine.

2013-10-17  Robert Dewar  <dewar@adacore.com>

	* sem_ch7.ads: Comment fixes.

2013-10-17  Robert Dewar  <dewar@adacore.com>

	* sem_ch7.adb (Analyze_Package_Specification): Remove circuit
	for ensuring that a package spec requires a body for some other
	reason than that it contains the declaration of an abstract state.

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

	* exp_ch11.adb (Expand_N_Raise_Expression): Fix call of
	Possible_Local_Raise.

2013-10-17  Thomas Quinot  <quinot@adacore.com>

	* exp_pakd.adb (Expand_Bit_Packed_Element_Set): Unchecked
	conversion of Or_Rhs to Etype of New_Rhs is required only when
	the latter is the result of a byte swap operation.

2013-10-17  Thomas Quinot  <quinot@adacore.com>

	* exp_dist.adb (Build_To_Any_Function): For a type with opaque
	representation that is not transmitted as an unconstrained value,
	use 'Write, not 'Output, to generate the opaque representation.

2013-10-17  Yannick Moy  <moy@adacore.com>

	* sem_res.adb (Resolve_Short_Circuit): Only
	generate expression-with-action when full expansion is set.

2013-10-17  Yannick Moy  <moy@adacore.com>

	* debug.adb Remove obsolete comment.

2013-10-17  Thomas Quinot  <quinot@adacore.com>

	* exp_ch4.adb (Process_Transient_Object.Find_Enclosing_Contexts):
	Avoid late insertion when expanding an expression with action
	nested within a transient block; Do not inconditionally generate
	a finalization call if the generated object is from a specific
	branch of a conditional expression.

2013-10-17  Pascal Obry  <obry@adacore.com>

	* g-arrspl.adb: Ensure Finalize call is idempotent.
	* g-arrspl.adb (Finalize): Makes the call idempotent.

From-SVN: r203767

gcc/ada/ChangeLog

+2013-10-17  Robert Dewar  <dewar@adacore.com>
+
+	* sem_prag.adb (Record_Possible_Body_Reference): Fix test for
+	being in body.
+	(Add_Constituent): Merged into Check_Refined_Global_Item.
+	(Check_Matching_Constituent): A constituent that has the proper Part_Of
+	option and comes from a private child or a sibling is now collected.
+	(Check_Matching_Modes): Merged into Check_Refined_Global_Item.
+	(Check_Refined_Global_Item): Code cleanup.
+	(Collect_Constituent): New routine.
+	(Inconsistent_Mode_Error): Moved out from Check_Matching_Modes.
+
+2013-10-17  Ed Schonberg  <schonberg@adacore.com>
+
+	* freeze.adb (Check_Current_Instance, Process): Add RM reference
+	and mention immutably limited types, when the current instance
+	is illegal in Ada 2012.
+
+2013-10-17  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_warn.adb (Check_Unused_Withs): If the main unit is a
+	subunit, apply the check to the units mentioned in its context
+	only. This provides additional warnings on with_clauses that
+	are superfluous.
+
+2013-10-17  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* sem_ch3.adb (Analyze_Declarations): Emit an
+	error message concerning state refinement when the spec defines at
+	least one non-null abstract state and the body's SPARK mode is On.
+	(Requires_State_Refinement): New routine.
+
+2013-10-17  Robert Dewar  <dewar@adacore.com>
+
+	* sem_ch7.ads: Comment fixes.
+
+2013-10-17  Robert Dewar  <dewar@adacore.com>
+
+	* sem_ch7.adb (Analyze_Package_Specification): Remove circuit
+	for ensuring that a package spec requires a body for some other
+	reason than that it contains the declaration of an abstract state.
+
+2013-10-17  Tristan Gingold  <gingold@adacore.com>
+
+	* exp_ch11.adb (Expand_N_Raise_Expression): Fix call of
+	Possible_Local_Raise.
+
+2013-10-17  Thomas Quinot  <quinot@adacore.com>
+
+	* exp_pakd.adb (Expand_Bit_Packed_Element_Set): Unchecked
+	conversion of Or_Rhs to Etype of New_Rhs is required only when
+	the latter is the result of a byte swap operation.
+
+2013-10-17  Thomas Quinot  <quinot@adacore.com>
+
+	* exp_dist.adb (Build_To_Any_Function): For a type with opaque
+	representation that is not transmitted as an unconstrained value,
+	use 'Write, not 'Output, to generate the opaque representation.
+
+2013-10-17  Yannick Moy  <moy@adacore.com>
+
+	* sem_res.adb (Resolve_Short_Circuit): Only
+	generate expression-with-action when full expansion is set.
+
+2013-10-17  Yannick Moy  <moy@adacore.com>
+
+	* debug.adb Remove obsolete comment.
+
+2013-10-17  Thomas Quinot  <quinot@adacore.com>
+
+	* exp_ch4.adb (Process_Transient_Object.Find_Enclosing_Contexts):
+	Avoid late insertion when expanding an expression with action
+	nested within a transient block; Do not inconditionally generate
+	a finalization call if the generated object is from a specific
+	branch of a conditional expression.
+
+2013-10-17  Pascal Obry  <obry@adacore.com>
+
+	* g-arrspl.adb: Ensure Finalize call is idempotent.
+	* g-arrspl.adb (Finalize): Makes the call idempotent.
+
 2013-10-17  Hristian Kirtchev  <kirtchev@adacore.com>
 
 	* sem_prag.adb (Is_Matching_Input): Account

gcc/ada/exp_ch11.adb

@@ -1450,7 +1450,7 @@ package body Exp_Ch11 is
       RCE : Node_Id;
 
    begin
-      Possible_Local_Raise (N, Name (N));
+      Possible_Local_Raise (N, Entity (Name (N)));
 
       --  Later we must teach the back end/gigi how to deal with this, but
       --  for now we will assume the type is Standard_Boolean and transform

gcc/ada/exp_dist.adb

@@ -9838,7 +9838,8 @@ package body Exp_Dist is
                --  Constrained and unconstrained array types
 
                declare
-                  Constrained : constant Boolean := Is_Constrained (Typ);
+                  Constrained : constant Boolean :=
+                    not Transmit_As_Unconstrained (Typ);
 
                   procedure TA_Ary_Add_Process_Element
                     (Stmts   : List_Id;
@@ -9957,16 +9958,29 @@ package body Exp_Dist is
 
                   --  Generate:
                   --    T'Output (Strm'Access, E);
+                  --  or
+                  --    T'Write (Strm'Access, E);
+                  --  depending on whether to transmit as unconstrained
 
-                  Append_To (Stms,
-                      Make_Attribute_Reference (Loc,
-                        Prefix         => New_Occurrence_Of (Typ, Loc),
-                        Attribute_Name => Name_Output,
-                        Expressions    => New_List (
-                          Make_Attribute_Reference (Loc,
-                            Prefix         => New_Occurrence_Of (Strm, Loc),
-                            Attribute_Name => Name_Access),
-                          New_Occurrence_Of (Expr_Parameter, Loc))));
+                  declare
+                     Attr_Name : Name_Id;
+                  begin
+                     if Transmit_As_Unconstrained (Typ) then
+                        Attr_Name := Name_Output;
+                     else
+                        Attr_Name := Name_Write;
+                     end if;
+
+                     Append_To (Stms,
+                         Make_Attribute_Reference (Loc,
+                           Prefix         => New_Occurrence_Of (Typ, Loc),
+                           Attribute_Name => Attr_Name,
+                           Expressions    => New_List (
+                             Make_Attribute_Reference (Loc,
+                               Prefix         => New_Occurrence_Of (Strm, Loc),
+                               Attribute_Name => Name_Access),
+                             New_Occurrence_Of (Expr_Parameter, Loc))));
+                  end;
 
                   --  Generate:
                   --    BS_To_Any (Strm, A);

gcc/ada/exp_pakd.adb

@@ -1703,11 +1703,17 @@ package body Exp_Pakd is
                   Set_Etype (New_Rhs, Etype (Left_Opnd (New_Rhs)));
                end if;
 
+               --  If New_Rhs has been byte swapped, need to convert Or_Rhs
+               --  to the return type of the byte swapping function now.
+
+               if Require_Byte_Swapping then
+                  Or_Rhs := Unchecked_Convert_To (Etype (New_Rhs), Or_Rhs);
+               end if;
+
                New_Rhs :=
                  Make_Op_Or (Loc,
                    Left_Opnd  => New_Rhs,
-                   Right_Opnd => Unchecked_Convert_To
-                                   (Etype (New_Rhs), Or_Rhs));
+                   Right_Opnd => Or_Rhs);
             end;
          end if;
 

gcc/ada/freeze.adb

@@ -1872,8 +1872,16 @@ package body Freeze is
                     and then Is_Type (Entity (Prefix (N)))
                     and then Entity (Prefix (N)) = E
                   then
-                     Error_Msg_N
-                       ("current instance must be a limited type", Prefix (N));
+                     if Ada_Version < Ada_2012 then
+                        Error_Msg_N
+                          ("current instance must be a limited type",
+                             Prefix (N));
+                     else
+                        Error_Msg_N
+                          ("current instance must be an immutably limited " &
+                            "type (RM-2012, 7.5 (8.1/3))",
+                             Prefix (N));
+                     end if;
                      return Abandon;
                   else
                      return OK;

gcc/ada/sem_ch3.adb

@@ -2071,6 +2071,12 @@ package body Sem_Ch3 is
       --  If the states have visible refinement, remove the visibility of each
       --  constituent at the end of the package body declarations.
 
+      function Requires_State_Refinement
+        (Spec_Id : Entity_Id;
+         Body_Id : Entity_Id) return Boolean;
+      --  Determine whether a package denoted by its spec and body entities
+      --  requires refinement of abstract states.
+
       -----------------
       -- Adjust_Decl --
       -----------------
@@ -2100,6 +2106,82 @@ package body Sem_Ch3 is
          end if;
       end Remove_Visible_Refinements;
 
+      -------------------------------
+      -- Requires_State_Refinement --
+      -------------------------------
+
+      function Requires_State_Refinement
+        (Spec_Id : Entity_Id;
+         Body_Id : Entity_Id) return Boolean
+      is
+         function Mode_Is_Off (Prag : Node_Id) return Boolean;
+         --  Given pragma SPARK_Mode, determine whether the mode is Off
+
+         -----------------
+         -- Mode_Is_Off --
+         -----------------
+
+         function Mode_Is_Off (Prag : Node_Id) return Boolean is
+            Mode : Node_Id;
+
+         begin
+            --  The default SPARK mode is On
+
+            if No (Prag) then
+               return False;
+            end if;
+
+            Mode :=
+              Get_Pragma_Arg (First (Pragma_Argument_Associations (Prag)));
+
+            --  Then the pragma lacks an argument, the default mode is On
+
+            if No (Mode) then
+               return False;
+            else
+               return Chars (Mode) = Name_Off;
+            end if;
+         end Mode_Is_Off;
+
+      --  Start of processing for Requires_State_Refinement
+
+      begin
+         --  A package that does not define at least one abstract state cannot
+         --  possibly require refinement.
+
+         if No (Abstract_States (Spec_Id)) then
+            return False;
+
+         --  The package instroduces a single null state which does not merit
+         --  refinement.
+
+         elsif Has_Null_Abstract_State (Spec_Id) then
+            return False;
+
+         --  Check whether the package body is subject to pragma SPARK_Mode. If
+         --  it is and the mode is Off, the package body is considered to be in
+         --  regular Ada and does not require refinement.
+
+         elsif Mode_Is_Off (SPARK_Mode_Pragmas (Body_Id)) then
+            return False;
+
+         --  The body's SPARK_Mode may be inherited from a similar pragma that
+         --  appears in the private declarations of the spec. The pragma we are
+         --  interested appears as the second entry in SPARK_Mode_Pragmas.
+
+         elsif Present (SPARK_Mode_Pragmas (Spec_Id))
+           and then Mode_Is_Off (Next_Pragma (SPARK_Mode_Pragmas (Spec_Id)))
+         then
+            return False;
+
+         --  The spec defines at least one abstract state and the body has no
+         --  way of circumventing the refinement.
+
+         else
+            return True;
+         end if;
+      end Requires_State_Refinement;
+
       --  Local variables
 
       Body_Id     : Entity_Id;
@@ -2264,9 +2346,7 @@ package body Sem_Ch3 is
             --  State refinement is required when the package declaration has
             --  abstract states. Null states are not considered.
 
-            elsif Present (Abstract_States (Spec_Id))
-              and then not Has_Null_Abstract_State (Spec_Id)
-            then
+            elsif Requires_State_Refinement (Spec_Id, Body_Id) then
                Error_Msg_NE
                  ("package & requires state refinement", Context, Spec_Id);
             end if;

gcc/ada/sem_ch7.adb

@@ -1493,34 +1493,6 @@ package body Sem_Ch7 is
 
       Check_One_Tagged_Type_Or_Extension_At_Most;
 
-      --  Issue an error if a package that is a library unit does not require a
-      --  body, and we have a non-null abstract state (SPARK LRM 7.1.5(4)).
-
-      if not Unit_Requires_Body (Id, Ignore_Abstract_State => True)
-        and then Present (Abstract_States (Id))
-
-        --  We use Scope_Depth of 1 to identify library units, which seems a
-        --  bit ugly, but there doesn't seem to be an easier way.
-
-        and then Scope_Depth (Id) = 1
-
-        --  A null abstract state always appears as the sole element of the
-        --  state list.
-
-        and then not Is_Null_State (Node (First_Elmt (Abstract_States (Id))))
-      then
-         declare
-            P : constant Node_Id := Get_Pragma (Id, Pragma_Abstract_State);
-         begin
-            Error_Msg_NE
-              ("package & specifies a non-null abstract state", P, Id);
-            Error_Msg_N
-              ("\but package does not otherwise require a body", P);
-            Error_Msg_N
-              ("\pragma Elaborate_Body is required in this case", P);
-         end;
-      end if;
-
       --  If switch set, output information on why body required
 
       if List_Body_Required_Info

gcc/ada/sem_ch7.ads

@@ -60,7 +60,10 @@ package Sem_Ch7 is
    --  Ignore_Abstract_State is set True, then the test for a non-null abstract
    --  state (which normally requires a body) is not carried out. This allows
    --  the use of this routine to tell if there is some other reason that a
-   --  body is required (as is required for analyzing Abstract_State).
+   --  body is required (as is required for analyzing Abstract_State). This
+   --  is not currently used, but may be useful in future if we implement a
+   --  compatibility mode which warns about possible incompatibilities if a
+   --  SPARK 2014 program is compiled with a SPARK-unaware compiler.
 
    procedure May_Need_Implicit_Body (E : Entity_Id);
    --  If a package declaration contains tasks or RACWs and does not require

gcc/ada/sem_warn.adb

@@ -2545,13 +2545,16 @@ package body Sem_Warn is
          return;
       end if;
 
-      --  Flag any unused with clauses, but skip this step if we are compiling
-      --  a subunit on its own, since we do not have enough information to
-      --  determine whether with's are used. We will get the relevant warnings
-      --  when we compile the parent. This is the normal style of GNAT
-      --  compilation in any case.
+      --  Flag any unused with clauses. For a subunit, check only the units
+      --  in its context, not those of the parent, which may be needed by other
+      --  subunits.  We will get the full warnings when we compile the parent,
+      --  but the following is helpful when compiling a subunit by itself.
 
       if Nkind (Unit (Cunit (Main_Unit))) = N_Subunit then
+         if Current_Sem_Unit = Main_Unit then
+            Check_One_Unit (Main_Unit);
+         end if;
+
          return;
       end if;