2016-06-20 Hristian Kirtchev <kirtchev@adacore.com>

	* s-regpat.adb, sem_prag.adb, pprint.adb, sem_ch13.adb: Minor
	reformatting.

2016-06-20  Tristan Gingold  <gingold@adacore.com>

	* make.adb (Check_Standard_Library): Consider system.ads
	if s-stalib.adb is not available.
	* gnatbind.adb (Add_Artificial_ALI_File): New procedure extracted from
	gnatbind.

2016-06-20  Thomas Quinot  <quinot@adacore.com>

	* g-socket.adb (Is_IP_Address): A string consisting in digits only is
	not a dotted quad.

2016-06-20  Arnaud Charlet  <charlet@adacore.com>

	* exp_ch7.adb (Build_Invariant_Procedure_Body):
	decorate invariant procedure body with typical properties of
	procedure entityes.

2016-06-20  Arnaud Charlet  <charlet@adacore.com>

	* a-exetim-darwin.adb: New file.



git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@237598 138bc75d-0d04-0410-961f-82ee72b054a4

10 files changed, 406 insertions, 109 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 9845111ed2b..5f5bd60253f 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,30 @@
+2016-06-20  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* s-regpat.adb, sem_prag.adb, pprint.adb, sem_ch13.adb: Minor
+	reformatting.
+
+2016-06-20  Tristan Gingold  <gingold@adacore.com>
+
+	* make.adb (Check_Standard_Library): Consider system.ads
+	if s-stalib.adb is not available.
+	* gnatbind.adb (Add_Artificial_ALI_File): New procedure extracted from
+	gnatbind.
+
+2016-06-20  Thomas Quinot  <quinot@adacore.com>
+
+	* g-socket.adb (Is_IP_Address): A string consisting in digits only is
+	not a dotted quad.
+
+2016-06-20  Arnaud Charlet  <charlet@adacore.com>
+
+	* exp_ch7.adb (Build_Invariant_Procedure_Body):
+	decorate invariant procedure body with typical properties of
+	procedure entityes.
+
+2016-06-20  Arnaud Charlet  <charlet@adacore.com>
+
+	* a-exetim-darwin.adb: New file.
+
 2016-06-16  Hristian Kirtchev  <kirtchev@adacore.com>
 
 	* atree.ads, atree.adb (Elist29): New routine.
diff --git a/gcc/ada/a-exetim-darwin.adb b/gcc/ada/a-exetim-darwin.adb
new file mode 100644
index 00000000000..36a657cadac
--- /dev/null
+++ b/gcc/ada/a-exetim-darwin.adb
@@ -0,0 +1,210 @@
+------------------------------------------------------------------------------
+--                                                                          --
+--                         GNAT RUN-TIME COMPONENTS                         --
+--                                                                          --
+--                   A D A . E X E C U T I O N _ T I M E                    --
+--                                                                          --
+--                                 B o d y                                  --
+--                                                                          --
+--         Copyright (C) 2007-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- --
+-- ware  Foundation;  either version 3,  or (at your option) any later ver- --
+-- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
+-- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
+-- or FITNESS FOR A PARTICULAR PURPOSE.                                     --
+--                                                                          --
+-- As a special exception under Section 7 of GPL version 3, you are granted --
+-- additional permissions described in the GCC Runtime Library Exception,   --
+-- version 3.1, as published by the Free Software Foundation.               --
+--                                                                          --
+-- You should have received a copy of the GNU General Public License and    --
+-- a copy of the GCC Runtime Library Exception along with this program;     --
+-- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
+-- <http://www.gnu.org/licenses/>.                                          --
+--                                                                          --
+-- GNAT was originally developed  by the GNAT team at  New York University. --
+-- Extensive contributions were provided by Ada Core Technologies Inc.      --
+--                                                                          --
+------------------------------------------------------------------------------
+
+--  This is the Darwin version of this package
+
+with Ada.Task_Identification;  use Ada.Task_Identification;
+with Ada.Unchecked_Conversion;
+
+with System.Tasking;
+with System.OS_Interface; use System.OS_Interface;
+with System.Task_Primitives.Operations; use System.Task_Primitives.Operations;
+
+with Interfaces.C; use Interfaces.C;
+
+package body Ada.Execution_Time is
+
+   ---------
+   -- "+" --
+   ---------
+
+   function "+"
+     (Left  : CPU_Time;
+      Right : Ada.Real_Time.Time_Span) return CPU_Time
+   is
+      use type Ada.Real_Time.Time;
+   begin
+      return CPU_Time (Ada.Real_Time.Time (Left) + Right);
+   end "+";
+
+   function "+"
+     (Left  : Ada.Real_Time.Time_Span;
+      Right : CPU_Time) return CPU_Time
+   is
+      use type Ada.Real_Time.Time;
+   begin
+      return CPU_Time (Left + Ada.Real_Time.Time (Right));
+   end "+";
+
+   ---------
+   -- "-" --
+   ---------
+
+   function "-"
+     (Left  : CPU_Time;
+      Right : Ada.Real_Time.Time_Span) return CPU_Time
+   is
+      use type Ada.Real_Time.Time;
+   begin
+      return CPU_Time (Ada.Real_Time.Time (Left) - Right);
+   end "-";
+
+   function "-"
+     (Left  : CPU_Time;
+      Right : CPU_Time) return Ada.Real_Time.Time_Span
+   is
+      use type Ada.Real_Time.Time;
+   begin
+      return (Ada.Real_Time.Time (Left) - Ada.Real_Time.Time (Right));
+   end "-";
+
+   -----------
+   -- Clock --
+   -----------
+
+   function Clock
+     (T : Ada.Task_Identification.Task_Id :=
+        Ada.Task_Identification.Current_Task) return CPU_Time
+   is
+      function Convert_Ids is new
+        Ada.Unchecked_Conversion (Task_Id, System.Tasking.Task_Id);
+
+      function To_CPU_Time is
+        new Ada.Unchecked_Conversion (Duration, CPU_Time);
+      --  Time is equal to Duration (although it is a private type) and
+      --  CPU_Time is equal to Time.
+
+      subtype integer_t is Interfaces.C.int;
+      subtype mach_port_t is integer_t;
+      --  Type definition for Mach.
+
+      type time_value_t is record
+         seconds : integer_t;
+         microseconds : integer_t;
+      end record;
+      pragma Convention (C, time_value_t);
+      --  Mach time_value_t
+
+      type thread_basic_info_t is record
+         user_time     : time_value_t;
+         system_time   : time_value_t;
+         cpu_usage     : integer_t;
+         policy        : integer_t;
+         run_state     : integer_t;
+         flags         : integer_t;
+         suspend_count : integer_t;
+         sleep_time    : integer_t;
+      end record;
+      pragma Convention (C, thread_basic_info_t);
+      --  Mach structure from thread_info.h
+
+      THREAD_BASIC_INFO       : constant := 3;
+      THREAD_BASIC_INFO_COUNT : constant := 10;
+      --  Flavors for basic info
+
+      function thread_info (Target : mach_port_t;
+                            Flavor : integer_t;
+                            Thread_Info : System.Address;
+                            Count : System.Address) return integer_t;
+      pragma Import (C, thread_info);
+      --  Mach call to get info on a thread
+
+      function pthread_mach_thread_np (Thread : pthread_t) return mach_port_t;
+      pragma Import (C, pthread_mach_thread_np);
+      --  Get Mach thread from posix thread
+
+      Result    : Interfaces.C.int;
+      Thread    : pthread_t;
+      Port      : mach_port_t;
+      Ti        : thread_basic_info_t;
+      Count     : integer_t;
+   begin
+      if T = Ada.Task_Identification.Null_Task_Id then
+         raise Program_Error;
+      end if;
+
+      Thread := Get_Thread_Id (Convert_Ids (T));
+      Port := pthread_mach_thread_np (Thread);
+      pragma Assert (Port > 0);
+
+      Count := THREAD_BASIC_INFO_COUNT;
+      Result := thread_info (Port, THREAD_BASIC_INFO,
+                             Ti'Address, Count'Address);
+      pragma Assert (Result = 0);
+      pragma Assert (Count = THREAD_BASIC_INFO_COUNT);
+
+      return To_CPU_Time
+        (Duration (Ti.user_time.seconds + Ti.system_time.seconds)
+           + Duration (Ti.user_time.microseconds
+                         + Ti.system_time.microseconds) / 1E6);
+   end Clock;
+
+   --------------------------
+   -- Clock_For_Interrupts --
+   --------------------------
+
+   function Clock_For_Interrupts return CPU_Time is
+   begin
+      --  According to AI 0170-1, D.14(18.1/3), if Interrupt_Clocks_Supported
+      --  is set to False the function raises Program_Error.
+
+      raise Program_Error;
+      return CPU_Time_First;
+   end Clock_For_Interrupts;
+
+   -----------
+   -- Split --
+   -----------
+
+   procedure Split
+     (T  : CPU_Time;
+      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;
+
+   -------------
+   -- Time_Of --
+   -------------
+
+   function Time_Of
+     (SC : Ada.Real_Time.Seconds_Count;
+      TS : Ada.Real_Time.Time_Span := Ada.Real_Time.Time_Span_Zero)
+      return CPU_Time
+   is
+   begin
+      return CPU_Time (Ada.Real_Time.Time_Of (SC, TS));
+   end Time_Of;
+
+end Ada.Execution_Time;
diff --git a/gcc/ada/exp_ch7.adb b/gcc/ada/exp_ch7.adb
index 0e6dc4591c2..c76d7af3708 100644
--- a/gcc/ada/exp_ch7.adb
+++ b/gcc/ada/exp_ch7.adb
@@ -4769,6 +4769,10 @@ package body Exp_Ch7 is
                 Statements => Stmts));
       Proc_Body_Id := Defining_Entity (Proc_Body);
 
+      Set_Ekind (Proc_Body_Id, E_Subprogram_Body);
+      Set_Etype (Proc_Body_Id, Standard_Void_Type);
+      Set_Scope (Proc_Body_Id, Scope (Typ));
+
       --  Link both spec and body to avoid generating duplicates
 
       Set_Corresponding_Body (Proc_Decl, Proc_Body_Id);
diff --git a/gcc/ada/g-socket.adb b/gcc/ada/g-socket.adb
index 6a61a810e39..a4a7d4f467d 100644
--- a/gcc/ada/g-socket.adb
+++ b/gcc/ada/g-socket.adb
@@ -150,7 +150,7 @@ package body GNAT.Sockets is
    --  Output an array of inet address components in hex or decimal mode
 
    function Is_IP_Address (Name : String) return Boolean;
-   --  Return true when Name is an IP address in standard dot notation
+   --  Return true when Name is an IPv4 address in dotted quad notation
 
    procedure Netdb_Lock;
    pragma Inline (Netdb_Lock);
@@ -996,7 +996,8 @@ package body GNAT.Sockets is
 
    function Get_Host_By_Name (Name : String) return Host_Entry_Type is
    begin
-      --  Detect IP address name and redirect to Inet_Addr
+      --  If the given name actually is the string representation of
+      --  an IP address, use Get_Host_By_Address instead.
 
       if Is_IP_Address (Name) then
          return Get_Host_By_Address (Inet_Addr (Name));
@@ -1503,16 +1504,37 @@ package body GNAT.Sockets is
    -------------------
 
    function Is_IP_Address (Name : String) return Boolean is
+      Dots : Natural := 0;
    begin
+      --  Perform a cursory check for a dotted quad: we must have 1 to 3
+      --  dots, and there must be at least one digit around each.
+
       for J in Name'Range loop
-         if Name (J) /= '.'
-           and then Name (J) not in '0' .. '9'
-         then
+         if Name (J) = '.' then
+
+            --  Check that the dot is not in first or last position, and
+            --  that it is followed by a digit. Note that we already know
+            --  that it is preceded by a digit, or we would have returned
+            --  earlier on.
+
+            if J in Name'First + 1 .. Name'Last - 1
+              and then Name (J + 1) in '0' .. '9'
+            then
+               Dots := Dots + 1;
+
+            else
+
+               --  Definitely not a proper dotted quad
+
+               return False;
+            end if;
+
+         elsif Name (J) not in '0' .. '9' then
             return False;
          end if;
       end loop;
 
-      return True;
+      return Dots in 1 .. 3;
    end Is_IP_Address;
 
    -------------
diff --git a/gcc/ada/gnatbind.adb b/gcc/ada/gnatbind.adb
index 3a4ec5318e0..1fa489a22df 100644
--- a/gcc/ada/gnatbind.adb
+++ b/gcc/ada/gnatbind.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- --
@@ -89,6 +89,9 @@ procedure Gnatbind is
    --  Table to record the sources in the closure, to avoid duplications. Used
    --  only with switch -R.
 
+   procedure Add_Artificial_ALI_File (Name : String);
+   --  Artificially add ALI file Name in the closure.
+
    function Gnatbind_Supports_Auto_Init return Boolean;
    --  Indicates if automatic initialization of elaboration procedure
    --  through the constructor mechanism is possible on the platform.
@@ -113,6 +116,30 @@ procedure Gnatbind is
    function Is_Cross_Compiler return Boolean;
    --  Returns True iff this is a cross-compiler
 
+   -----------------------------
+   -- Add_Artificial_ALI_File --
+   -----------------------------
+
+   procedure Add_Artificial_ALI_File (Name : String) is
+      Id : ALI_Id;
+      pragma Warnings (Off, Id);
+   begin
+      Name_Len := Name'Length;
+      Name_Buffer (1 .. Name_Len) := Name;
+      Std_Lib_File := Name_Find;
+      Text := Read_Library_Info (Std_Lib_File, True);
+
+      Id :=
+        Scan_ALI
+          (F             => Std_Lib_File,
+           T             => Text,
+           Ignore_ED     => False,
+           Err           => False,
+           Ignore_Errors => Debug_Flag_I);
+
+      Free (Text);
+   end Add_Artificial_ALI_File;
+
    ---------------------------------
    -- Gnatbind_Supports_Auto_Init --
    ---------------------------------
@@ -740,29 +767,15 @@ begin
 
       --  Add System.Standard_Library to list to ensure that these files are
       --  included in the bind, even if not directly referenced from Ada code
-      --  This is suppressed if the appropriate targparm switch is set.
+      --  This is suppressed if the appropriate targparm switch is set. Be sure
+      --  in any case that System is in the closure, as it may contains linker
+      --  options. Note that it will be automatically added if s-stalib is
+      --  added.
 
       if not Suppress_Standard_Library_On_Target then
-         Name_Buffer (1 .. 12) := "s-stalib.ali";
-         Name_Len := 12;
-         Std_Lib_File := Name_Find;
-         Text := Read_Library_Info (Std_Lib_File, True);
-
-         declare
-            Id : ALI_Id;
-            pragma Warnings (Off, Id);
-
-         begin
-            Id :=
-              Scan_ALI
-                (F             => Std_Lib_File,
-                 T             => Text,
-                 Ignore_ED     => False,
-                 Err           => False,
-                 Ignore_Errors => Debug_Flag_I);
-         end;
-
-         Free (Text);
+         Add_Artificial_ALI_File ("s-stalib.ali");
+      else
+         Add_Artificial_ALI_File ("system.ali");
       end if;
 
       --  Load ALIs for all dependent units
diff --git a/gcc/ada/make.adb b/gcc/ada/make.adb
index 4449ef13f98..c0bde7365b7 100644
--- a/gcc/ada/make.adb
+++ b/gcc/ada/make.adb
@@ -84,8 +84,11 @@ package body Make is
    --  Make control characters visible
 
    Standard_Library_Package_Body_Name : constant String := "s-stalib.adb";
-   --  Every program depends on this package, that must then be checked,
-   --  especially when -f and -a are used.
+   System_Package_Spec_Name : constant String := "system.ads";
+   --  Every program depends on one of these packages: usually the first one,
+   --  or if Supress_Standard_Library is true on the second one. The dependency
+   --  is not always explicit and considering it is important when -f and -a
+   --  are used.
 
    type Sigint_Handler is access procedure;
    pragma Convention (C, Sigint_Handler);
@@ -2701,39 +2704,43 @@ package body Make is
       begin
          Need_To_Check_Standard_Library := False;
 
+         Name_Len := 0;
+
          if not Targparm.Suppress_Standard_Library_On_Target then
-            declare
-               Sfile  : File_Name_Type;
-               Add_It : Boolean := True;
+            Add_Str_To_Name_Buffer (Standard_Library_Package_Body_Name);
+         else
+            Add_Str_To_Name_Buffer (System_Package_Spec_Name);
+         end if;
 
-            begin
-               Name_Len := 0;
-               Add_Str_To_Name_Buffer (Standard_Library_Package_Body_Name);
-               Sfile := Name_Enter;
+         declare
+            Sfile  : File_Name_Type;
+            Add_It : Boolean := True;
 
-               --  If we have a special runtime, we add the standard
-               --  library only if we can find it.
+         begin
+            Sfile := Name_Enter;
 
-               if RTS_Switch then
-                  Add_It := Full_Source_Name (Sfile) /= No_File;
-               end if;
+            --  If we have a special runtime, we add the standard library only
+            --  if we can find it.
 
-               if Add_It then
-                  if not Queue.Insert
-                           ((Format  => Format_Gnatmake,
-                             File    => Sfile,
-                             Unit    => No_Unit_Name,
-                             Project => No_Project,
-                             Index   => 0,
-                             Sid     => No_Source))
-                  then
-                     if Is_In_Obsoleted (Sfile) then
-                        Executable_Obsolete := True;
-                     end if;
+            if RTS_Switch then
+               Add_It := Full_Source_Name (Sfile) /= No_File;
+            end if;
+
+            if Add_It then
+               if not Queue.Insert
+                        ((Format  => Format_Gnatmake,
+                          File    => Sfile,
+                          Unit    => No_Unit_Name,
+                          Project => No_Project,
+                          Index   => 0,
+                          Sid     => No_Source))
+               then
+                  if Is_In_Obsoleted (Sfile) then
+                     Executable_Obsolete := True;
                   end if;
                end if;
-            end;
-         end if;
+            end if;
+         end;
       end Check_Standard_Library;
 
       -----------------------------------
diff --git a/gcc/ada/pprint.adb b/gcc/ada/pprint.adb
index 1319f87f6fe..c520cf56116 100644
--- a/gcc/ada/pprint.adb
+++ b/gcc/ada/pprint.adb
@@ -555,8 +555,8 @@ package body Pprint is
 
                if not Is_Scalar_Type (Etype (Expr))
                  or else not Is_Scalar_Type (Etype (Expression (Expr)))
-                 or else Is_Modular_Integer_Type (Etype (Expr))
-                         /= Is_Modular_Integer_Type (Etype (Expression (Expr)))
+                 or else Is_Modular_Integer_Type (Etype (Expr)) /=
+                           Is_Modular_Integer_Type (Etype (Expression (Expr)))
                then
                   return Expr_Name (Subtype_Mark (Expr)) &
                     "(" & Expr_Name (Expression (Expr)) & ")";
diff --git a/gcc/ada/s-regpat.adb b/gcc/ada/s-regpat.adb
index 7675f70b1aa..f27639b978a 100644
--- a/gcc/ada/s-regpat.adb
+++ b/gcc/ada/s-regpat.adb
@@ -2614,10 +2614,15 @@ package body System.Regpat is
                   exit State_Machine when Input_Pos /= BOL_Pos;
 
                when EOL =>
+
                   --  A combination of MEOL and SEOL
+
                   if (Self.Flags and Multiple_Lines) = 0 then
-                     --  single line mode
+
+                     --  Single line mode
+
                      exit State_Machine when Input_Pos <= Data'Last;
+
                   elsif Input_Pos <= Last_In_Data then
                      exit State_Machine when Data (Input_Pos) /= ASCII.LF;
                   else
@@ -2632,9 +2637,11 @@ package body System.Regpat is
                   end if;
 
                when SEOL =>
-                  --  If we have a character before Data'Last (even if
-                  --  Last_In_Data stops before then), we can't have
-                  --  the end of the line.
+
+                  --  If there is a character before Data'Last (even if
+                  --  Last_In_Data stops before then), we can't have the
+                  --  end of the line.
+
                   exit State_Machine when Input_Pos <= Data'Last;
 
                when BOUND | NBOUND =>
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index 3e1ddb48a94..009bf3235f4 100644
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -13721,10 +13721,10 @@ package body Sem_Ch13 is
          declare
             T : UC_Entry renames Unchecked_Conversions.Table (N);
 
+            Act_Unit : constant Entity_Id  := T.Act_Unit;
             Eloc     : constant Source_Ptr := T.Eloc;
             Source   : constant Entity_Id  := T.Source;
             Target   : constant Entity_Id  := T.Target;
-            Act_Unit : constant Entity_Id  := T.Act_Unit;
 
             Source_Siz : Uint;
             Target_Siz : Uint;
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 6c7539bb494..902d1fc7885 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -23304,85 +23304,92 @@ package body Sem_Prag is
      (N         : Node_Id;
       Freeze_Id : Entity_Id := Empty)
    is
-      --  Local variables
-
-      Subp_Decl : constant Node_Id   := Find_Related_Declaration_Or_Body (N);
-      Spec_Id   : constant Entity_Id := Unique_Defining_Entity (Subp_Decl);
-      Expr      : constant Node_Id   := Expression (Get_Argument (N, Spec_Id));
+      Disp_Typ : Entity_Id;
+      --  The dispatching type of the subprogram subject to the pre- or
+      --  postcondition.
 
-      Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
-
-      Errors        : Nat;
-      Disp_Typ      : Entity_Id;
-      Restore_Scope : Boolean := False;
-
-      function Check_References (N : Node_Id) return Traverse_Result;
-      --  Check that the expression does not mention non-primitives of
-      --  the type, global objects of the type, or other illegalities
-      --  described and implied by AI12-0113.
+      function Check_References (Nod : Node_Id) return Traverse_Result;
+      --  Check that expression Nod does not mention non-primitives of the
+      --  type, global objects of the type, or other illegalities described
+      --  and implied by AI12-0113.
 
       ----------------------
       -- Check_References --
       ----------------------
 
-      function Check_References (N : Node_Id) return Traverse_Result is
+      function Check_References (Nod : Node_Id) return Traverse_Result is
       begin
-         if Nkind (N) = N_Function_Call
-           and then Is_Entity_Name (Name (N))
+         if Nkind (Nod) = N_Function_Call
+           and then Is_Entity_Name (Name (Nod))
          then
             declare
-               Func : constant Entity_Id := Entity (Name (N));
+               Func : constant Entity_Id := Entity (Name (Nod));
                Form : Entity_Id;
-            begin
 
-               --  An operation of the type must be a primitive.
+            begin
+               --  An operation of the type must be a primitive
 
                if No (Find_Dispatching_Type (Func)) then
                   Form := First_Formal (Func);
                   while Present (Form) loop
                      if Etype (Form) = Disp_Typ then
-                        Error_Msg_NE ("operation in class-wide condition "
-                          & "must be primitive of&", N, Disp_Typ);
+                        Error_Msg_NE
+                          ("operation in class-wide condition must be "
+                           & "primitive of &", Nod, Disp_Typ);
                      end if;
+
                      Next_Formal (Form);
                   end loop;
 
-                  --  A return object of the type is illegal as well.
+                  --  A return object of the type is illegal as well
 
                   if Etype (Func) = Disp_Typ
                     or else Etype (Func) = Class_Wide_Type (Disp_Typ)
                   then
-                     Error_Msg_NE ("operation in class-wide condition "
-                       & "must be primitive of&", N, Disp_Typ);
+                     Error_Msg_NE
+                       ("operation in class-wide condition must be primitive "
+                        & "of &", Nod, Disp_Typ);
                   end if;
                end if;
             end;
 
-         elsif Is_Entity_Name (N)
+         elsif Is_Entity_Name (Nod)
            and then
-             (Etype (N) = Disp_Typ
-               or else Etype (N) = Class_Wide_Type (Disp_Typ))
-           and then Ekind_In (Entity (N),  E_Variable, E_Constant)
+             (Etype (Nod) = Disp_Typ
+               or else Etype (Nod) = Class_Wide_Type (Disp_Typ))
+           and then Ekind_In (Entity (Nod), E_Constant, E_Variable)
          then
             Error_Msg_NE
-              ("object in class-wide condition must be formal of type&",
-                N, Disp_Typ);
-
-         elsif Nkind (N) = N_Explicit_Dereference
-           and then (Etype (N) = Disp_Typ
-               or else Etype (N) = Class_Wide_Type (Disp_Typ))
-           and then (not Is_Entity_Name (Prefix (N))
-             or else not Is_Formal (Entity (Prefix (N))))
+              ("object in class-wide condition must be formal of type &",
+                Nod, Disp_Typ);
+
+         elsif Nkind (Nod) = N_Explicit_Dereference
+           and then (Etype (Nod) = Disp_Typ
+                      or else Etype (Nod) = Class_Wide_Type (Disp_Typ))
+           and then (not Is_Entity_Name (Prefix (Nod))
+                      or else not Is_Formal (Entity (Prefix (Nod))))
          then
-            Error_Msg_NE ("operation in class-wide condition "
-              & "must be primitive of&", N, Disp_Typ);
+            Error_Msg_NE
+              ("operation in class-wide condition must be primitive of &",
+               Nod, Disp_Typ);
          end if;
 
          return OK;
       end Check_References;
 
-      procedure Check_Class_Wide_Condition is new
-        Traverse_Proc (Check_References);
+      procedure Check_Class_Wide_Condition is
+        new Traverse_Proc (Check_References);
+
+      --  Local variables
+
+      Subp_Decl : constant Node_Id   := Find_Related_Declaration_Or_Body (N);
+      Spec_Id   : constant Entity_Id := Unique_Defining_Entity (Subp_Decl);
+      Expr      : constant Node_Id   := Expression (Get_Argument (N, Spec_Id));
+
+      Save_Ghost_Mode : constant Ghost_Mode_Type := Ghost_Mode;
+
+      Errors        : Nat;
+      Restore_Scope : Boolean := False;
 
    --  Start of processing for Analyze_Pre_Post_Condition_In_Decl_Part
 
@@ -23451,9 +23458,9 @@ package body Sem_Prag is
                   & "of a tagged type", N);
             end if;
 
-         else
-            --  Remaining semantic checks require a full tree traversal.
+         --  Remaining semantic checks require a full tree traversal
 
+         else
             Check_Class_Wide_Condition (Expr);
          end if;
 
@@ -26490,8 +26497,8 @@ package body Sem_Prag is
             --  overridings between them.
 
             while Present (Decl) loop
-               if Nkind_In (Decl,
-                  N_Subprogram_Declaration, N_Abstract_Subprogram_Declaration)
+               if Nkind_In (Decl, N_Abstract_Subprogram_Declaration,
+                                  N_Subprogram_Declaration)
                then
                   Prim := Defining_Entity (Decl);