[multiple changes]

2016-07-07  Ed Schonberg  <schonberg@adacore.com>

	* sem_prag.ads, sem_prag.adb (Build_Classwide_Expression): Include
	overridden operation as parameter, in order to map formals of
	the overridden and overring operation properly prior to rewriting
	the inherited condition.
	* freeze.adb (Check_Inherited_Cnonditions): Change call to
	Build_Class_Wide_Expression accordingly.  In Spark_Mode, add
	call to analyze the contract of the parent operation, prior to
	mapping formals between operations.

2016-07-07  Arnaud Charlet  <charlet@adacore.com>

	* adabkend.adb (Scan_Back_End_Switches): Ignore -o/-G switches
	as done in back_end.adb.
	(Scan_Compiler_Args): Remove special case for CodePeer/SPARK, no longer
	needed, and prevents proper handling of multi-unit sources.

2016-07-07  Thomas Quinot  <quinot@adacore.com>

	* g-sechas.adb, g-sechas.ads (GNAT.Secure_Hashes.H): Add Hash_Stream
	type with Write primitive calling Update on the underlying context
	(and dummy Read primitive raising P_E).

2016-07-07  Thomas Quinot  <quinot@adacore.com>

	* sem_ch13.adb: Minor reformatting.

From-SVN: r238111

8 files changed, 171 insertions, 103 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 828932c..d4e6482 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,31 @@
+2016-07-07  Ed Schonberg  <schonberg@adacore.com>
+
+	* sem_prag.ads, sem_prag.adb (Build_Classwide_Expression): Include
+	overridden operation as parameter, in order to map formals of
+	the overridden and overring operation properly prior to rewriting
+	the inherited condition.
+	* freeze.adb (Check_Inherited_Cnonditions): Change call to
+	Build_Class_Wide_Expression accordingly.  In Spark_Mode, add
+	call to analyze the contract of the parent operation, prior to
+	mapping formals between operations.
+
+2016-07-07  Arnaud Charlet  <charlet@adacore.com>
+
+	* adabkend.adb (Scan_Back_End_Switches): Ignore -o/-G switches
+	as done in back_end.adb.
+	(Scan_Compiler_Args): Remove special case for CodePeer/SPARK, no longer
+	needed, and prevents proper handling of multi-unit sources.
+
+2016-07-07  Thomas Quinot  <quinot@adacore.com>
+
+	* g-sechas.adb, g-sechas.ads (GNAT.Secure_Hashes.H): Add Hash_Stream
+	type with Write primitive calling Update on the underlying context
+	(and dummy Read primitive raising P_E).
+
+2016-07-07  Thomas Quinot  <quinot@adacore.com>
+
+	* sem_ch13.adb: Minor reformatting.
+
 2016-07-07  Thomas Quinot  <quinot@adacore.com>
 
 	* g-socket.ads: Document performance consideration for stream
diff --git a/gcc/ada/adabkend.adb b/gcc/ada/adabkend.adb
index e850923..7eee887 100644
--- a/gcc/ada/adabkend.adb
+++ b/gcc/ada/adabkend.adb
@@ -98,31 +98,15 @@ package body Adabkend is
          --  affect code generation or falling through if it does, so the
          --  switch will get stored.
 
-         if Is_Internal_GCC_Switch (Switch_Chars) then
+         --  Skip -o, -G or internal GCC switches together with their argument.
+
+         if Switch_Chars (First .. Last) = "o"
+           or else Switch_Chars (First .. Last) = "G"
+           or else Is_Internal_GCC_Switch (Switch_Chars)
+         then
             Next_Arg := Next_Arg + 1;
             return; -- ignore this switch
 
-         --  Record that an object file name has been specified. The actual
-         --  file name argument is picked up and saved below by the main body
-         --  of Scan_Compiler_Arguments.
-
-         elsif Switch_Chars (First .. Last) = "o" then
-            if First = Last then
-               if Opt.Output_File_Name_Present then
-
-                  --  Ignore extra -o when -gnatO has already been specified
-
-                  Next_Arg := Next_Arg + 1;
-
-               else
-                  Opt.Output_File_Name_Present := True;
-               end if;
-
-               return;
-            else
-               Fail ("invalid switch: " & Switch_Chars);
-            end if;
-
          --  Set optimization indicators appropriately. In gcc-based GNAT this
          --  is picked up from imported variables set by the gcc driver, but
          --  for compilers with non-gcc back ends we do it here to allow use
@@ -244,16 +228,6 @@ package body Adabkend is
             then
                if Is_Switch (Argv) then
                   Fail ("Object file name missing after -gnatO");
-
-               --  In GNATprove_Mode, such an object file is never written, and
-               --  the call to Set_Output_Object_File_Name may fail (e.g. when
-               --  the object file name does not have the expected suffix).
-               --  So we skip that call when GNATprove_Mode is set. Same for
-               --  CodePeer_Mode.
-
-               elsif GNATprove_Mode or CodePeer_Mode then
-                  Output_File_Name_Seen := True;
-
                else
                   Set_Output_Object_File_Name (Argv);
                   Output_File_Name_Seen := True;
diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb
index 6962d9b..9b94fce 100644
--- a/gcc/ada/freeze.adb
+++ b/gcc/ada/freeze.adb
@@ -23,51 +23,52 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
-with Aspects;  use Aspects;
-with Atree;    use Atree;
-with Checks;   use Checks;
-with Debug;    use Debug;
-with Einfo;    use Einfo;
-with Elists;   use Elists;
-with Errout;   use Errout;
-with Exp_Ch3;  use Exp_Ch3;
-with Exp_Ch7;  use Exp_Ch7;
-with Exp_Disp; use Exp_Disp;
-with Exp_Pakd; use Exp_Pakd;
-with Exp_Util; use Exp_Util;
-with Exp_Tss;  use Exp_Tss;
-with Fname;    use Fname;
-with Ghost;    use Ghost;
-with Layout;   use Layout;
-with Lib;      use Lib;
-with Namet;    use Namet;
-with Nlists;   use Nlists;
-with Nmake;    use Nmake;
-with Opt;      use Opt;
-with Restrict; use Restrict;
-with Rident;   use Rident;
-with Rtsfind;  use Rtsfind;
-with Sem;      use Sem;
-with Sem_Aux;  use Sem_Aux;
-with Sem_Cat;  use Sem_Cat;
-with Sem_Ch6;  use Sem_Ch6;
-with Sem_Ch7;  use Sem_Ch7;
-with Sem_Ch8;  use Sem_Ch8;
-with Sem_Ch13; use Sem_Ch13;
-with Sem_Eval; use Sem_Eval;
-with Sem_Mech; use Sem_Mech;
-with Sem_Prag; use Sem_Prag;
-with Sem_Res;  use Sem_Res;
-with Sem_Util; use Sem_Util;
-with Sinfo;    use Sinfo;
-with Snames;   use Snames;
-with Stand;    use Stand;
-with Targparm; use Targparm;
-with Tbuild;   use Tbuild;
-with Ttypes;   use Ttypes;
-with Uintp;    use Uintp;
-with Urealp;   use Urealp;
-with Warnsw;   use Warnsw;
+with Aspects;   use Aspects;
+with Atree;     use Atree;
+with Checks;    use Checks;
+with Contracts; use Contracts;
+with Debug;     use Debug;
+with Einfo;     use Einfo;
+with Elists;    use Elists;
+with Errout;    use Errout;
+with Exp_Ch3;   use Exp_Ch3;
+with Exp_Ch7;   use Exp_Ch7;
+with Exp_Disp;  use Exp_Disp;
+with Exp_Pakd;  use Exp_Pakd;
+with Exp_Util;  use Exp_Util;
+with Exp_Tss;   use Exp_Tss;
+with Fname;     use Fname;
+with Ghost;     use Ghost;
+with Layout;    use Layout;
+with Lib;       use Lib;
+with Namet;     use Namet;
+with Nlists;    use Nlists;
+with Nmake;     use Nmake;
+with Opt;       use Opt;
+with Restrict;  use Restrict;
+with Rident;    use Rident;
+with Rtsfind;   use Rtsfind;
+with Sem;       use Sem;
+with Sem_Aux;   use Sem_Aux;
+with Sem_Cat;   use Sem_Cat;
+with Sem_Ch6;   use Sem_Ch6;
+with Sem_Ch7;   use Sem_Ch7;
+with Sem_Ch8;   use Sem_Ch8;
+with Sem_Ch13;  use Sem_Ch13;
+with Sem_Eval;  use Sem_Eval;
+with Sem_Mech;  use Sem_Mech;
+with Sem_Prag;  use Sem_Prag;
+with Sem_Res;   use Sem_Res;
+with Sem_Util;  use Sem_Util;
+with Sinfo;     use Sinfo;
+with Snames;    use Snames;
+with Stand;     use Stand;
+with Targparm;  use Targparm;
+with Tbuild;    use Tbuild;
+with Ttypes;    use Ttypes;
+with Uintp;     use Uintp;
+with Urealp;    use Urealp;
+with Warnsw;    use Warnsw;
 
 package body Freeze is
 
@@ -1417,6 +1418,16 @@ package body Freeze is
             --  overriding operations.
 
             if SPARK_Mode = On then
+
+               --  Analyze the contract items of the parent operation, before
+               --  they are rewritten when inherited.
+
+               Analyze_Entry_Or_Subprogram_Contract
+                 (Overridden_Operation (Prim));
+
+               --  Now verify the legality of inherited contracts for LSP
+               --  conformance.
+
                Collect_Inherited_Class_Wide_Conditions (Prim);
             end if;
          end if;
@@ -1440,15 +1451,15 @@ package body Freeze is
             A_Pre    := Find_Aspect (Par_Prim, Aspect_Pre);
 
             if Present (A_Pre) and then Class_Present (A_Pre) then
-               Build_Classwide_Expression (Expression (A_Pre), Prim,
-                                           Adjust_Sloc => False);
+               Build_Classwide_Expression
+                 (Expression (A_Pre), Prim, Par_Prim, Adjust_Sloc => False);
             end if;
 
             A_Post := Find_Aspect (Par_Prim, Aspect_Post);
 
             if Present (A_Post) and then Class_Present (A_Post) then
-               Build_Classwide_Expression (Expression (A_Post), Prim,
-                                           Adjust_Sloc => False);
+               Build_Classwide_Expression
+                 (Expression (A_Post), Prim, Par_Prim, Adjust_Sloc => False);
             end if;
          end if;
 
diff --git a/gcc/ada/g-sechas.adb b/gcc/ada/g-sechas.adb
index 0e70b5d..f2e8d5d 100644
--- a/gcc/ada/g-sechas.adb
+++ b/gcc/ada/g-sechas.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 2009-2014, Free Software Foundation, Inc.         --
+--          Copyright (C) 2009-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- --
@@ -341,6 +341,20 @@ package body GNAT.Secure_Hashes is
          end return;
       end HMAC_Initial_Context;
 
+      ----------
+      -- Read --
+      ----------
+
+      procedure Read
+        (Stream : in out Hash_Stream;
+         Item   : out Stream_Element_Array;
+         Last   : out Stream_Element_Offset)
+      is
+         pragma Unreferenced (Stream, Item, Last);
+      begin
+         raise Program_Error with "Hash_Stream is write-only";
+      end Read;
+
       ------------
       -- Update --
       ------------
@@ -364,7 +378,6 @@ package body GNAT.Secure_Hashes is
                C.M_State.Last := 0;
             end if;
          end loop;
-
       end Update;
 
       ------------
@@ -422,6 +435,18 @@ package body GNAT.Secure_Hashes is
          return Digest (C);
       end Wide_Digest;
 
+      -----------
+      -- Write --
+      -----------
+
+      procedure Write
+         (Stream : in out Hash_Stream;
+          Item   : Stream_Element_Array)
+      is
+      begin
+         Update (Stream.C.all, Item);
+      end Write;
+
    end H;
 
    -------------------------
diff --git a/gcc/ada/g-sechas.ads b/gcc/ada/g-sechas.ads
index c00150e..33e635c 100644
--- a/gcc/ada/g-sechas.ads
+++ b/gcc/ada/g-sechas.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 2009-2014, Free Software Foundation, Inc.         --
+--          Copyright (C) 2009-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- --
@@ -191,6 +191,12 @@ package GNAT.Secure_Hashes is
       --  Wide_Update) on a default initialized Context, followed by Digest
       --  on the resulting Context.
 
+      type Hash_Stream (C : access Context) is
+        new Root_Stream_Type with private;
+      --  Stream wrapper converting Write calls to Update calls on C.
+      --  Arbitrary data structures can thus be conveniently hashed using
+      --  their stream attributes.
+
    private
 
       Block_Length : constant Natural := Block_Words * Word_Length;
@@ -215,6 +221,20 @@ package GNAT.Secure_Hashes is
       Initial_Context : constant Context (KL => 0) := (others => <>);
       --  Initial values are provided by default initialization of Context
 
+      type Hash_Stream (C : access Context) is
+        new Root_Stream_Type with null record;
+
+      procedure Read
+        (Stream : in out Hash_Stream;
+         Item   : out Stream_Element_Array;
+         Last   : out Stream_Element_Offset);
+      --  Raise Program_Error: hash streams are write-only
+
+      procedure Write
+         (Stream : in out Hash_Stream;
+          Item   : Stream_Element_Array);
+      --  Call Update
+
    end H;
 
 end GNAT.Secure_Hashes;
diff --git a/gcc/ada/sem_ch13.adb b/gcc/ada/sem_ch13.adb
index 89a17c8..c0ff2ed 100644
--- a/gcc/ada/sem_ch13.adb
+++ b/gcc/ada/sem_ch13.adb
@@ -3823,8 +3823,8 @@ package body Sem_Ch13 is
       U_Ent : Entity_Id;
       --  The underlying entity to which the attribute applies. Generally this
       --  is the Underlying_Type of Ent, except in the case where the clause
-      --  applies to full view of incomplete type or private type in which case
-      --  U_Ent is just a copy of Ent.
+      --  applies to the full view of an incomplete or private type, in which
+      --  case U_Ent is just a copy of Ent.
 
       FOnly : Boolean := False;
       --  Reset to True for subtype specific attribute (Alignment, Size)
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index f603e317..6e86b1c 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -26396,8 +26396,12 @@ package body Sem_Prag is
    procedure Build_Classwide_Expression
      (Prag        : Node_Id;
       Subp        : Entity_Id;
+      Par_Subp    : Entity_Id;
       Adjust_Sloc : Boolean)
    is
+      Par_Formal  : Entity_Id;
+      Subp_Formal : Entity_Id;
+
       function Replace_Entity (N : Node_Id) return Traverse_Result;
       --  Replace reference to formal of inherited operation or to primitive
       --  operation of root type, with corresponding entity for derived type,
@@ -26503,6 +26507,17 @@ package body Sem_Prag is
    --  Start of processing for Build_Classwide_Expression
 
    begin
+      --  Add mapping from old formals to new formals.
+
+      Par_Formal := First_Formal (Par_Subp);
+      Subp_Formal  := First_Formal (Subp);
+
+      while Present (Par_Formal) and then Present (Subp_Formal) loop
+         Primitives_Mapping.Set (Par_Formal, Subp_Formal);
+         Next_Formal (Par_Formal);
+         Next_Formal (Subp_Formal);
+      end loop;
+
       Replace_Condition_Entities (Prag);
    end Build_Classwide_Expression;
 
@@ -26555,10 +26570,8 @@ package body Sem_Prag is
       Loc          : constant Source_Ptr := Sloc (Prag);
       Prag_Nam     : constant Name_Id    := Pragma_Name (Prag);
       Check_Prag   : Node_Id;
-      Inher_Formal : Entity_Id;
       Msg_Arg      : Node_Id;
       Nam          : Name_Id;
-      Subp_Formal  : Entity_Id;
 
    --  Start of processing for Build_Pragma_Check_Equivalent
 
@@ -26573,16 +26586,6 @@ package body Sem_Prag is
 
          Update_Primitives_Mapping (Inher_Id, Subp_Id);
 
-         --  Add mapping from old formals to new formals.
-
-         Inher_Formal := First_Formal (Inher_Id);
-         Subp_Formal  := First_Formal (Subp_Id);
-         while Present (Inher_Formal) and then Present (Subp_Formal) loop
-            Primitives_Mapping.Set (Inher_Formal, Subp_Formal);
-            Next_Formal (Inher_Formal);
-            Next_Formal (Subp_Formal);
-         end loop;
-
          --  Use generic machinery to copy inherited pragma, as if it were an
          --  instantiation, resetting source locations appropriately, so that
          --  expressions inside the inherited pragma use chained locations.
@@ -26592,9 +26595,13 @@ package body Sem_Prag is
          Set_Copied_Sloc_For_Inherited_Pragma
            (Unit_Declaration_Node (Subp_Id), Inher_Id);
          Check_Prag := New_Copy_Tree (Source => Prag);
-         Build_Classwide_Expression (Check_Prag, Subp_Id, Adjust_Sloc => True);
 
-      --  Otherwise simply copy the original pragma
+         --  Build the inherited classwide condition.
+
+         Build_Classwide_Expression
+           (Check_Prag, Subp_Id, Inher_Id, Adjust_Sloc => True);
+
+      --  If not an inherited condition simply copy the original pragma
 
       else
          Check_Prag := New_Copy_Tree (Source => Prag);
@@ -29301,7 +29308,8 @@ package body Sem_Prag is
       Subp_Id  : Entity_Id)
    is
       function Overridden_Ancestor (S : Entity_Id) return Entity_Id;
-      --  ??? what does this routine do?
+      --  Locate the primitive operation with the name of S whose controlling
+      --  type is the dispatching type of Inher_Id.
 
       -------------------------
       -- Overridden_Ancestor --
@@ -29333,7 +29341,7 @@ package body Sem_Prag is
       Old_Prim : Entity_Id;
       Prim     : Entity_Id;
 
-   --  Start of processing for Primitive_Mapping
+   --  Start of processing for Update_Primitives_Mapping
 
    begin
       --  If the types are already in the map, it has been previously built for
diff --git a/gcc/ada/sem_prag.ads b/gcc/ada/sem_prag.ads
index 9a951ff..16ff72d 100644
--- a/gcc/ada/sem_prag.ads
+++ b/gcc/ada/sem_prag.ads
@@ -247,10 +247,12 @@ package Sem_Prag is
    procedure Build_Classwide_Expression
      (Prag        : Node_Id;
       Subp        : Entity_Id;
+      Par_Subp    : Entity_Id;
       Adjust_Sloc : Boolean);
    --  Build the expression for an inherited classwide condition. Prag is
    --  the pragma constructed from the corresponding aspect of the parent
-   --  subprogram, and Subp is the overridding operation. Adjust_Sloc is True
+   --  subprogram, and Subp is the overridding operation and Par_Subp is
+   --  the overridden operation that has the condition. Adjust_Sloc is True
    --  when the sloc of nodes traversed should be adjusted for the inherited
    --  pragma. The routine is also called to check whether an inherited
    --  operation that is not overridden but has inherited conditions need