[multiple changes]

2017-01-23  Yannick Moy  <moy@adacore.com>

	* frontend.adb (Frontend): Do not load runtime
	unit for GNATprove when parsing failed.
	* exp_ch9.adb: minor removal of extra whitespace
	* exp_ch6.adb: minor typo in comment
	* sem_util.adb: Code cleanup.
	* exp_ch9.ads, par-ch2.adb: minor style fixes in whitespace and comment
	* a-ngcefu.adb: minor style fix in whitespace

2017-01-23  Thomas Quinot  <quinot@adacore.com>

	* scos.ads: Document usage of 'd' as default SCO kind for
	declarations.
	* par_sco.adb (Traverse_Declarations_Or_Statements.
	Traverse_Degenerate_Subprogram): New supporting routine for expression
	functions and null procedures.
	(Traverse_Declarations_Or_Statements.Traverse_One): Add
	N_Expression_Function to the subprogram case; add required
	support for null procedures and expression functions.

2017-01-23  Bob Duff  <duff@adacore.com>

	* namet.ads (Bounded_String): Decrease the size of type
	Bounded_String to avoid running out of stack space.
	* namet.ads (Append): Don't ignore buffer overflow; raise
	Program_Error instead.

From-SVN: r244789

gcc/ada/ChangeLog

+2017-01-23  Yannick Moy  <moy@adacore.com>
+
+	* frontend.adb (Frontend): Do not load runtime
+	unit for GNATprove when parsing failed.
+	* exp_ch9.adb: minor removal of extra whitespace
+	* exp_ch6.adb: minor typo in comment
+	* sem_util.adb: Code cleanup.
+	* exp_ch9.ads, par-ch2.adb: minor style fixes in whitespace and comment
+	* a-ngcefu.adb: minor style fix in whitespace
+
+2017-01-23  Thomas Quinot  <quinot@adacore.com>
+
+	* scos.ads: Document usage of 'd' as default SCO kind for
+	declarations.
+	* par_sco.adb (Traverse_Declarations_Or_Statements.
+	Traverse_Degenerate_Subprogram): New supporting routine for expression
+	functions and null procedures.
+	(Traverse_Declarations_Or_Statements.Traverse_One): Add
+	N_Expression_Function to the subprogram case; add required
+	support for null procedures and expression functions.
+
+2017-01-23  Bob Duff  <duff@adacore.com>
+
+	* namet.ads (Bounded_String): Decrease the size of type
+	Bounded_String to avoid running out of stack space.
+	* namet.ads (Append): Don't ignore buffer overflow; raise
+	Program_Error instead.
+
 2017-01-23  Hristian Kirtchev  <kirtchev@adacore.com>
 
 	* exp_ch5.adb, freeze.adb, par-ch4.adb, scng.adb, sem_ch13.adb,

gcc/ada/a-ngcefu.adb

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2015, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2016, 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- --

gcc/ada/exp_ch6.adb

@@ -6073,7 +6073,7 @@ package body Exp_Ch6 is
       --  Exp_Ch9.Build_Simple_Entry_Call. The call is intra-object only if the
       --  subprogram being called is in the protected body being compiled, and
       --  if the protected object in the call is statically the enclosing type.
-      --  The object may be an component of some other data structure, in which
+      --  The object may be a component of some other data structure, in which
       --  case this must be handled as an inter-object call.
 
       if not In_Open_Scopes (Scop)

gcc/ada/exp_ch9.ads

@@ -273,7 +273,7 @@ package Exp_Ch9 is
    --  is the entity for the corresponding protected type declaration.
 
    function External_Subprogram (E : Entity_Id) return Entity_Id;
-   --  return the external version of a protected operation, which locks
+   --  Return the external version of a protected operation, which locks
    --  the object before invoking the internal protected subprogram body.
 
    function Find_Master_Scope (E : Entity_Id) return Entity_Id;

gcc/ada/frontend.adb

@@ -463,9 +463,12 @@ begin
       end if;
    end if;
 
-   --  In GNATprove mode, force the loading of a few RTE units
+   --  In GNATprove mode, force the loading of a few RTE units. This step is
+   --  skipped if we had a fatal error during parsing.
 
-   if GNATprove_Mode then
+   if GNATprove_Mode
+     and then Fatal_Error (Main_Unit) /= Error_Detected
+   then
       declare
          Unused : Entity_Id;
 

gcc/ada/namet.adb

@@ -115,10 +115,12 @@ package body Namet is
 
    procedure Append (Buf : in out Bounded_String; C : Character) is
    begin
-      if Buf.Length < Buf.Chars'Last then
+      if Buf.Length >= Buf.Chars'Last then
+         raise Program_Error;
+      end if;
+
       Buf.Length := Buf.Length + 1;
       Buf.Chars (Buf.Length) := C;
-      end if;
    end Append;
 
    procedure Append (Buf : in out Bounded_String; V : Nat) is

gcc/ada/namet.ads

@@ -31,7 +31,6 @@
 
 with Alloc;
 with Table;
-with Hostparm; use Hostparm;
 with System;   use System;
 with Types;    use Types;
 
@@ -149,9 +148,9 @@ package Namet is
 --  and the Boolean field is initialized to False, when a new Name table entry
 --  is created.
 
-   type Bounded_String (Max_Length : Natural := 4 * Max_Line_Length) is limited
-   --  The default here is intended to be an infinite value that ensures that
-   --  we never overflow the buffer (names this long are too absurd to worry).
+   type Bounded_String (Max_Length : Natural := 2**12) is limited
+   --  It's unlikely to have names longer than this. But we don't want to make
+   --  it too big, because we declare these on the stack in recursive routines.
    record
       Length : Natural := 0;
       Chars  : String (1 .. Max_Length);

gcc/ada/par_sco.adb

@@ -1440,7 +1440,10 @@ package body Par_SCO is
       --  This routine is logically the same as Process_Decisions, except that
       --  the arguments are saved in the SD table for later processing when
       --  Set_Statement_Entry is called, which goes through the saved entries
-      --  making the corresponding calls to Process_Decision.
+      --  making the corresponding calls to Process_Decision. Note: the
+      --  enclosing statement must have already been added to the current
+      --  statement sequence, so that nested decisions are properly
+      --  identified as such.
 
       procedure Process_Decisions_Defer (L : List_Id; T : Character);
       pragma Inline (Process_Decisions_Defer);
@@ -1457,6 +1460,10 @@ package body Par_SCO is
       procedure Traverse_Aspects (N : Node_Id);
       --  Helper for Traverse_One: traverse N's aspect specifications
 
+      procedure Traverse_Degenerate_Subprogram (N : Node_Id);
+      --  Common code to handle null procedures and expression functions.
+      --  Emit a SCO of the given Kind and N outside of the dominance flow.
+
       -------------------------------
       -- Extend_Statement_Sequence --
       -------------------------------
@@ -1514,6 +1521,9 @@ package body Par_SCO is
                   To_Node := Defining_Identifier (N);
                end if;
 
+            when N_Subexpr =>
+               To_Node := N;
+
             when others =>
                null;
          end case;
@@ -1720,6 +1730,44 @@ package body Par_SCO is
          end loop;
       end Traverse_Aspects;
 
+      ------------------------------------
+      -- Traverse_Degenerate_Subprogram --
+      ------------------------------------
+
+      procedure Traverse_Degenerate_Subprogram (N : Node_Id) is
+      begin
+         --  Complete current sequence of statements
+
+         Set_Statement_Entry;
+
+         declare
+            Saved_Dominant : constant Dominant_Info := Current_Dominant;
+            --  Save last statement in current sequence as dominant
+
+         begin
+            --  Output statement SCO for degenerate subprogram body
+            --  (null statement or freestanding expression) outside of
+            --  the dominance chain.
+
+            Current_Dominant := No_Dominant;
+            Extend_Statement_Sequence (N, Typ => ' ');
+
+            --  For the case of an expression-function, collect decisions
+            --  embedded in the expression now.
+
+            if Nkind (N) in N_Subexpr then
+               Process_Decisions_Defer (N, 'X');
+            end if;
+            Set_Statement_Entry;
+
+            --  Restore current dominant information designating last
+            --  statement in previous sequence (i.e. make the dominance
+            --  chain skip over the degenerate body).
+
+            Current_Dominant := Saved_Dominant;
+         end;
+      end Traverse_Degenerate_Subprogram;
+
       ------------------
       -- Traverse_One --
       ------------------
@@ -1755,9 +1803,30 @@ package body Par_SCO is
 
             when N_Subprogram_Body_Stub
                | N_Subprogram_Declaration
+               | N_Expression_Function
             =>
+               declare
+                  Spec : constant Node_Id := Specification (N);
+               begin
                   Process_Decisions_Defer
-                 (Parameter_Specifications (Specification (N)), 'X');
+                    (Parameter_Specifications (Spec), 'X');
+
+                  --  Case of a null procedure: generate a NULL statement SCO
+
+                  if Nkind (N) = N_Subprogram_Declaration
+                    and then Nkind (Spec) = N_Procedure_Specification
+                    and then Null_Present (Spec)
+                  then
+                     Traverse_Degenerate_Subprogram (N);
+
+                  --  Case of an expression function: generate a statement
+                  --  SCO for the expression (and then decision SCOs for any
+                  --  nested decisions).
+
+                  elsif Nkind (N) = N_Expression_Function then
+                     Traverse_Degenerate_Subprogram (Expression (N));
+                  end if;
+               end;
 
             --  Entry declaration
 

gcc/ada/scos.ads

@@ -152,6 +152,7 @@ package SCOs is
    --      o        object declaration
    --      r        renaming declaration
    --      i        generic instantiation
+   --      d        any other kind of declaration
    --      A        ACCEPT statement (from ACCEPT to end of parameter profile)
    --      C        CASE statement (from CASE to end of expression)
    --      E        EXIT statement

gcc/ada/sem_util.adb

@@ -9344,17 +9344,8 @@ package body Sem_Util is
          --  The implicit case lacks all property pragmas
 
          elsif No (AR) and then No (AW) and then No (ER) and then No (EW) then
-
-            --  A variable of a protected type only has the properties
-            --  Async_Readers and Async_Writers. It cannot have Part_Of
-            --  components (only protected objects can), hence it cannot
-            --  inherit their properties Effective_Reads and Effective_Writes.
-            --  (SPARK RM 7.1.2(16))
-
             if Is_Protected_Type (Etype (Item_Id)) then
-               return
-                 Property = Name_Async_Readers
-                   or else Property = Name_Async_Writers;
+               return Protected_Object_Has_Enabled_Property;
             else
                return True;
             end if;