[multiple changes]

2017-09-25  Yannick Moy  <moy@adacore.com>

	* exp_spark.adb (Expand_SPARK_Indexed_Component,
	Expand_SPARK_Selected_Component): New procedures to insert explicit
	dereference if required.
	(Expand_SPARK): Call the new procedures.

2017-09-25  Patrick Bernardi  <bernardi@adacore.com>

	* libgnat/a-stwiun.adb, libgnat/s-stchop__vxworks.adb,
	libgnat/g-socthi__vxworks.ads, libgnat/a-stzunb.adb,
	libgnat/a-strunb.adb, libgnarl/s-osinte__lynxos178.adb,
	libgnarl/s-intman__vxworks.adb, libgnarl/s-osinte__darwin.adb,
	libgnarl/a-exetim__darwin.adb: Removed ineffective use-clauses.

2017-09-25  Vasiliy Fofanov  <fofanov@adacore.com>

	* adaint.c (win32_wait): Properly handle error and take into account
	the WIN32 limitation on the number of simultaneous wait objects.

2017-09-25  Yannick Moy  <moy@adacore.com>

	* sem_ch3.adb (Constant_Redeclaration): Do not insert a call to the
	invariant procedure in GNATprove mode.
	* sem_ch5.adb (Analyze_Assignment): Likewise.

From-SVN: r253143

gcc/ada/ChangeLog

+2017-09-25  Yannick Moy  <moy@adacore.com>
+
+	* exp_spark.adb (Expand_SPARK_Indexed_Component,
+	Expand_SPARK_Selected_Component): New procedures to insert explicit
+	dereference if required.
+	(Expand_SPARK): Call the new procedures.
+
+2017-09-25  Patrick Bernardi  <bernardi@adacore.com>
+
+	* libgnat/a-stwiun.adb, libgnat/s-stchop__vxworks.adb,
+	libgnat/g-socthi__vxworks.ads, libgnat/a-stzunb.adb,
+	libgnat/a-strunb.adb, libgnarl/s-osinte__lynxos178.adb,
+	libgnarl/s-intman__vxworks.adb, libgnarl/s-osinte__darwin.adb,
+	libgnarl/a-exetim__darwin.adb: Removed ineffective use-clauses.
+
+2017-09-25  Vasiliy Fofanov  <fofanov@adacore.com>
+
+	* adaint.c (win32_wait): Properly handle error and take into account
+	the WIN32 limitation on the number of simultaneous wait objects.
+
+2017-09-25  Yannick Moy  <moy@adacore.com>
+
+	* sem_ch3.adb (Constant_Redeclaration): Do not insert a call to the
+	invariant procedure in GNATprove mode.
+	* sem_ch5.adb (Analyze_Assignment): Likewise.
+
 2017-09-25  Piotr Trojanek  <trojanek@adacore.com>
 
 	* adabkend.adb (Call_Back_End): Fix wording of "front-end" and

gcc/ada/adaint.c

@@ -2551,6 +2551,7 @@ win32_wait (int *status)
   DWORD res;
   int hl_len;
   int found;
+  int pos;
 
  START_WAIT:
 
@@ -2563,7 +2564,15 @@ win32_wait (int *status)
   /* -------------------- critical section -------------------- */
   EnterCS();
 
+  /* ??? We can't wait for more than MAXIMUM_WAIT_OBJECTS due to a Win32
+     limitation */
+  if (plist_length < MAXIMUM_WAIT_OBJECTS)
   hl_len = plist_length;
+  else
+    {
+      errno = EINVAL;
+      return -1;
+    }
 
 #ifdef CERT
   hl = (HANDLE *) xmalloc (sizeof (HANDLE) * hl_len);
@@ -2586,6 +2595,13 @@ win32_wait (int *status)
 
   res = WaitForMultipleObjects (hl_len, hl, FALSE, INFINITE);
 
+  /* If there was an error, exit now */
+  if (res == WAIT_FAILED)
+    {
+      errno = EINVAL;
+      return -1;
+    }
+
   /* if the ProcListEvt has been signaled then the list of processes has been
      updated to add or remove a handle, just loop over */
 
@@ -2596,9 +2612,17 @@ win32_wait (int *status)
       goto START_WAIT;
     }
 
-  h = hl[res - WAIT_OBJECT_0];
+  /* Handle two distinct groups of return codes: finished waits and abandoned
+     waits */
+
+  if (res < WAIT_ABANDONED_0)
+    pos = res - WAIT_OBJECT_0;
+  else
+    pos = res - WAIT_ABANDONED_0;
+
+  h = hl[pos];
   GetExitCodeProcess (h, &exitcode);
-  pid = pidl [res - WAIT_OBJECT_0];
+  pid = pidl [pos];
 
   found = __gnat_win32_remove_handle (h, -1);
 

gcc/ada/exp_spark.adb

@@ -58,6 +58,9 @@ package body Exp_SPARK is
    procedure Expand_SPARK_Freeze_Type (E : Entity_Id);
    --  Build the DIC procedure of a type when needed, if not already done
 
+   procedure Expand_SPARK_Indexed_Component (N : Node_Id);
+   --  Insert explicit dereference if required
+
    procedure Expand_SPARK_N_Object_Declaration (N : Node_Id);
    --  Perform object-declaration-specific expansion
 
@@ -67,6 +70,9 @@ package body Exp_SPARK is
    procedure Expand_SPARK_Op_Ne (N : Node_Id);
    --  Rewrite operator /= based on operator = when defined explicitly
 
+   procedure Expand_SPARK_Selected_Component (N : Node_Id);
+   --  Insert explicit dereference if required
+
    ------------------
    -- Expand_SPARK --
    ------------------
@@ -138,6 +144,12 @@ package body Exp_SPARK is
                Expand_SPARK_Freeze_Type (Entity (N));
             end if;
 
+         when N_Indexed_Component =>
+            Expand_SPARK_Indexed_Component (N);
+
+         when N_Selected_Component =>
+            Expand_SPARK_Selected_Component (N);
+
          --  In SPARK mode, no other constructs require expansion
 
          when others =>
@@ -264,6 +276,20 @@ package body Exp_SPARK is
       end if;
    end Expand_SPARK_Freeze_Type;
 
+   ------------------------------------
+   -- Expand_SPARK_Indexed_Component --
+   ------------------------------------
+
+   procedure Expand_SPARK_Indexed_Component (N : Node_Id) is
+      P   : constant Node_Id    := Prefix (N);
+      T   : constant Entity_Id  := Etype (P);
+   begin
+      if Is_Access_Type (T) then
+         Insert_Explicit_Dereference (P);
+         Analyze_And_Resolve (P, Designated_Type (T));
+      end if;
+   end Expand_SPARK_Indexed_Component;
+
    ---------------------------------------
    -- Expand_SPARK_N_Object_Declaration --
    ---------------------------------------
@@ -445,4 +471,31 @@ package body Exp_SPARK is
       end if;
    end Expand_SPARK_Potential_Renaming;
 
+   -------------------------------------
+   -- Expand_SPARK_Selected_Component --
+   -------------------------------------
+
+   procedure Expand_SPARK_Selected_Component (N : Node_Id) is
+      P    : constant Node_Id   := Prefix (N);
+      Ptyp : constant Entity_Id := Underlying_Type (Etype (P));
+   begin
+      if Present (Ptyp)
+        and then Is_Access_Type (Ptyp)
+      then
+         --  First set prefix type to proper access type, in case it currently
+         --  has a private (non-access) view of this type.
+
+         Set_Etype (P, Ptyp);
+
+         Insert_Explicit_Dereference (P);
+         Analyze_And_Resolve (P, Designated_Type (Ptyp));
+
+         if Ekind (Etype (P)) = E_Private_Subtype
+           and then Is_For_Access_Subtype (Etype (P))
+         then
+            Set_Etype (P, Base_Type (Etype (P)));
+         end if;
+      end if;
+   end Expand_SPARK_Selected_Component;
+
 end Exp_SPARK;

gcc/ada/libgnarl/a-exetim__darwin.adb

@@ -189,7 +189,6 @@ package body Ada.Execution_Time is
       SC : out Ada.Real_Time.Seconds_Count;
       TS : out Ada.Real_Time.Time_Span)
    is
-      use type Ada.Real_Time.Time;
    begin
       Ada.Real_Time.Split (Ada.Real_Time.Time (T), SC, TS);
    end Split;

gcc/ada/libgnarl/s-intman__vxworks.adb

@@ -37,7 +37,6 @@
 package body System.Interrupt_Management is
 
    use System.OS_Interface;
-   use type Interfaces.C.int;
 
    -----------------------
    -- Local Subprograms --

gcc/ada/libgnarl/s-osinte__darwin.adb

@@ -39,7 +39,6 @@ with Interfaces.C.Extensions;
 
 package body System.OS_Interface is
    use Interfaces.C;
-   use Interfaces.C.Extensions;
 
    -----------------
    -- To_Duration --

gcc/ada/libgnarl/s-osinte__lynxos178.adb

@@ -37,8 +37,6 @@ pragma Polling (Off);
 
 package body System.OS_Interface is
 
-   use Interfaces.C;
-
    ------------------
    --  Current_CPU --
    ------------------

gcc/ada/libgnat/a-strunb.adb

@@ -35,8 +35,6 @@ with Ada.Unchecked_Deallocation;
 
 package body Ada.Strings.Unbounded is
 
-   use Ada.Finalization;
-
    ---------
    -- "&" --
    ---------

gcc/ada/libgnat/a-stwiun.adb

@@ -35,8 +35,6 @@ with Ada.Unchecked_Deallocation;
 
 package body Ada.Strings.Wide_Unbounded is
 
-   use Ada.Finalization;
-
    ---------
    -- "&" --
    ---------

gcc/ada/libgnat/a-stzunb.adb

@@ -35,8 +35,6 @@ with Ada.Unchecked_Deallocation;
 
 package body Ada.Strings.Wide_Wide_Unbounded is
 
-   use Ada.Finalization;
-
    ---------
    -- "&" --
    ---------

gcc/ada/libgnat/g-socthi__vxworks.ads

@@ -49,8 +49,6 @@ package GNAT.Sockets.Thin is
 
    package C renames Interfaces.C;
 
-   use type System.CRTL.ssize_t;
-
    function Socket_Errno return Integer renames GNAT.OS_Lib.Errno;
    --  Returns last socket error number
 

gcc/ada/libgnat/s-stchop__vxworks.adb

@@ -103,8 +103,6 @@ package body System.Stack_Checking.Operations is
    --------------------------------------
 
    procedure Set_Stack_Limit_For_Current_Task is
-      use Interfaces.C;
-
       type OS_Stack_Info is record
          Size  : Interfaces.C.int;
          Base  : System.Address;

gcc/ada/sem_ch3.adb

@@ -12755,9 +12755,13 @@ package body Sem_Ch3 is
          end if;
 
          --  A deferred constant is a visible entity. If type has invariants,
-         --  verify that the initial value satisfies them.
+         --  verify that the initial value satisfies them. This is not done in
+         --  GNATprove mode, as GNATprove handles invariant checks itself.
 
-         if Has_Invariants (T) and then Present (Invariant_Procedure (T)) then
+         if Has_Invariants (T)
+           and then Present (Invariant_Procedure (T))
+           and then not GNATprove_Mode
+         then
             Insert_After (N,
               Make_Invariant_Call (New_Occurrence_Of (Prev, Sloc (N))));
          end if;

gcc/ada/sem_ch5.adb

@@ -839,14 +839,16 @@ package body Sem_Ch5 is
          Set_Referenced_Modified (Lhs, Out_Param => False);
       end if;
 
-      --  RM 7.3.2 (12/3): An assignment to a view conversion (from a type
-      --  to one of its ancestors) requires an invariant check. Apply check
-      --  only if expression comes from source, otherwise it will be applied
-      --  when value is assigned to source entity.
+      --  RM 7.3.2 (12/3): An assignment to a view conversion (from a type to
+      --  one of its ancestors) requires an invariant check. Apply check only
+      --  if expression comes from source, otherwise it will be applied when
+      --  value is assigned to source entity. This is not done in GNATprove
+      --  mode, as GNATprove handles invariant checks itself.
 
       if Nkind (Lhs) = N_Type_Conversion
         and then Has_Invariants (Etype (Expression (Lhs)))
         and then Comes_From_Source (Expression (Lhs))
+        and then not GNATprove_Mode
       then
          Insert_After (N, Make_Invariant_Call (Expression (Lhs)));
       end if;