[multiple changes]

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

	* exp_spark.adb (Expand_SPARK_Potential_Renaming): Fix sloc of copied
	subtree.

2017-01-12  Justin Squirek  <squirek@adacore.com>

	* exp_attr.adb (Expand_N_Attribute_Reference):
	Fix Finalization_Size case by properly resolving the type after
	rewritting the node.

2017-01-12  Hristian Kirtchev  <kirtchev@adacore.com>

	* exp_util.adb (Build_DIC_Procedure_Body): Semi-insert the body into
	the tree.
	(Build_DIC_Procedure_Declaration): Semi-insert the body into the tree.
	* binde.adb, exp_ch5.adb, sem_type.adb, sem.ads, sem_res.adb,
	exp_sel.ads: Minor reformatting.

2017-01-12  Justin Squirek  <squirek@adacore.com>

	* exp_ch6.adb (Expand_Call): Add guard to prevent
	invariant checks from being created for internally generated
	subprograms.

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

	* lib-writ.ads: Remove incorrect comment.

2017-01-12  Javier Miranda  <miranda@adacore.com>

	* debug.adb (-gnatd.K): Enable generation of contract-only
	procedures in CodePeer mode.
	* contracts.adb (Build_And_Analyze_Contract_Only_Subprograms):
	New subprogram.
	(Analyze_Contracts): Generate contract-only procedures if -gnatdK is
	set.
	* scil_ll.ads, scil_ll.adb (Get_Contract_Only_Body_Name): New
	subprogram.
	(Get_Contract_Only_Missing_Body_Name): New subprogram.
	(Get_Contract_Only_Body): New subprogram.
	(Set_Contract_Only_Body): New subprogram.
	(Is_Contract_Only_Body): New subprogram.
	(Set_Is_Contract_Only_Body): New subprogram.
	(SCIL_Nodes): Replace table by hash-table.

From-SVN: r244356

16 files changed, 873 insertions, 101 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 787b324..048b975 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,49 @@
+2017-01-12  Yannick Moy  <moy@adacore.com>
+
+	* exp_spark.adb (Expand_SPARK_Potential_Renaming): Fix sloc of copied
+	subtree.
+
+2017-01-12  Justin Squirek  <squirek@adacore.com>
+
+	* exp_attr.adb (Expand_N_Attribute_Reference):
+	Fix Finalization_Size case by properly resolving the type after
+	rewritting the node.
+
+2017-01-12  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* exp_util.adb (Build_DIC_Procedure_Body): Semi-insert the body into
+	the tree.
+	(Build_DIC_Procedure_Declaration): Semi-insert the body into the tree.
+	* binde.adb, exp_ch5.adb, sem_type.adb, sem.ads, sem_res.adb,
+	exp_sel.ads: Minor reformatting.
+
+2017-01-12  Justin Squirek  <squirek@adacore.com>
+
+	* exp_ch6.adb (Expand_Call): Add guard to prevent
+	invariant checks from being created for internally generated
+	subprograms.
+
+2017-01-12  Bob Duff  <duff@adacore.com>
+
+	* lib-writ.ads: Remove incorrect comment.
+
+2017-01-12  Javier Miranda  <miranda@adacore.com>
+
+	* debug.adb (-gnatd.K): Enable generation of contract-only
+	procedures in CodePeer mode.
+	* contracts.adb (Build_And_Analyze_Contract_Only_Subprograms):
+	New subprogram.
+	(Analyze_Contracts): Generate contract-only procedures if -gnatdK is
+	set.
+	* scil_ll.ads, scil_ll.adb (Get_Contract_Only_Body_Name): New
+	subprogram.
+	(Get_Contract_Only_Missing_Body_Name): New subprogram.
+	(Get_Contract_Only_Body): New subprogram.
+	(Set_Contract_Only_Body): New subprogram.
+	(Is_Contract_Only_Body): New subprogram.
+	(Set_Is_Contract_Only_Body): New subprogram.
+	(SCIL_Nodes): Replace table by hash-table.
+
 2017-01-12  Hristian Kirtchev  <kirtchev@adacore.com>
 
 	* exp_ch6.adb: Minor reformatting.
diff --git a/gcc/ada/binde.adb b/gcc/ada/binde.adb
index 7baf685..f655bf2 100644
--- a/gcc/ada/binde.adb
+++ b/gcc/ada/binde.adb
@@ -1211,14 +1211,18 @@ package body Binde is
       --  There is a lot of fiddly string manipulation below, because we don't
       --  want to depend on misc utility packages like Ada.Characters.Handling.
 
-      function Read_File (Name : String) return String_Ptr;
-      --  Read the entire contents of the named file
-
       function Get_Line return String;
       --  Read the next line from the file content read by Read_File. Strip
       --  leading and trailing blanks. Convert "(spec)" or "(body)" to
       --  "%s"/"%b". Remove comments (Ada style; "--" to end of line).
 
+      function Read_File (Name : String) return String_Ptr;
+      --  Read the entire contents of the named file
+
+      ---------------
+      -- Read_File --
+      ---------------
+
       function Read_File (Name : String) return String_Ptr is
          --  All of the following calls should succeed, because we checked the
          --  file in Switch.B, but we double check and raise Program_Error on
@@ -1232,9 +1236,11 @@ package body Binde is
          end if;
 
          declare
-            Len : constant Natural := Natural (File_Length (F));
-            Result : constant String_Ptr := new String (1 .. Len);
-            Len_Read : constant Natural := Read (F, Result (1)'Address, Len);
+            Len      : constant Natural    := Natural (File_Length (F));
+            Result   : constant String_Ptr := new String (1 .. Len);
+            Len_Read : constant Natural    :=
+                         Read (F, Result (1)'Address, Len);
+
             Status : Boolean;
 
          begin
@@ -1252,12 +1258,17 @@ package body Binde is
          end;
       end Read_File;
 
-      S : String_Ptr := Read_File (Force_Elab_Order_File.all);
-      Cur : Positive := 1;
+      Cur : Positive   := 1;
+      S   : String_Ptr := Read_File (Force_Elab_Order_File.all);
+
+      --------------
+      -- Get_Line --
+      --------------
 
       function Get_Line return String is
          First : Positive := Cur;
-         Last : Natural;
+         Last  : Natural;
+
       begin
          --  Skip to end of line
 
@@ -1293,12 +1304,16 @@ package body Binde is
          --  again.
 
          declare
+            Body_String : constant String   := "(body)";
+            BL          : constant Positive := Body_String'Length;
+            Spec_String : constant String   := "(spec)";
+            SL          : constant Positive := Spec_String'Length;
+
             Line : String renames S (First .. Last);
-            Spec_String : constant String := "(spec)";
-            SL : constant Positive := Spec_String'Length;
-            Body_String : constant String := "(body)";
-            BL : constant Positive := Body_String'Length;
-            Is_Spec, Is_Body : Boolean := False;
+
+            Is_Body : Boolean := False;
+            Is_Spec : Boolean := False;
+
          begin
             if Line'Length >= SL
               and then Line (Last - SL + 1 .. Last) = Spec_String
@@ -1336,8 +1351,12 @@ package body Binde is
          end;
       end Get_Line;
 
+      --  Local variables
+
       Empty_Name : constant Unit_Name_Type := Name_Find ("");
-      Prev_Unit : Unit_Id := No_Unit_Id;
+      Prev_Unit  : Unit_Id := No_Unit_Id;
+
+   --  Start of processing for Force_Elab_Order
 
    begin
       --  Loop through the file content, and build a dependency link for each
diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb
index fbfc684..e4e25bf 100644
--- a/gcc/ada/contracts.adb
+++ b/gcc/ada/contracts.adb
@@ -25,6 +25,7 @@
 
 with Aspects;  use Aspects;
 with Atree;    use Atree;
+with Debug;    use Debug;
 with Einfo;    use Einfo;
 with Elists;   use Elists;
 with Errout;   use Errout;
@@ -47,10 +48,16 @@ with Sem_Util; use Sem_Util;
 with Sinfo;    use Sinfo;
 with Snames;   use Snames;
 with Stringt;  use Stringt;
+with SCIL_LL;  use SCIL_LL;
 with Tbuild;   use Tbuild;
 
 package body Contracts is
 
+   procedure Build_And_Analyze_Contract_Only_Subprograms (L : List_Id);
+   --  (CodePeer): Subsidiary procedure to Analyze_Contracts which builds the
+   --  contract-only subprogram body of eligible subprograms found in L, adds
+   --  them to their corresponding list of declarations, and analyzes them.
+
    procedure Analyze_Contracts
      (L          : List_Id;
       Freeze_Nod : Node_Id;
@@ -345,6 +352,10 @@ package body Contracts is
 
    procedure Analyze_Contracts (L : List_Id) is
    begin
+      if CodePeer_Mode and then Debug_Flag_Dot_KK then
+         Build_And_Analyze_Contract_Only_Subprograms (L);
+      end if;
+
       Analyze_Contracts (L, Freeze_Nod => Empty, Freeze_Id => Empty);
    end Analyze_Contracts;
 
@@ -389,7 +400,7 @@ package body Contracts is
               (Obj_Id    => Defining_Entity (Decl),
                Freeze_Id => Freeze_Id);
 
-         --  Protected untis
+         --  Protected units
 
          elsif Nkind_In (Decl, N_Protected_Type_Declaration,
                                N_Single_Protected_Declaration)
@@ -2643,4 +2654,566 @@ package body Contracts is
       Pop_Scope;
    end Save_Global_References_In_Contract;
 
+   -------------------------------------------------
+   -- Build_And_Analyze_Contract_Only_Subprograms --
+   -------------------------------------------------
+
+   procedure Build_And_Analyze_Contract_Only_Subprograms (L : List_Id) is
+      procedure Analyze_Contract_Only_Subprograms (L : List_Id);
+      --  Analyze the contract-only subprograms of L
+
+      procedure Append_Contract_Only_Subprograms (Subp_List : List_Id);
+      --  Append the contract-only bodies of Subp_List to its declarations list
+
+      function Build_Contract_Only_Subprogram (E : Entity_Id) return Node_Id;
+      --  If E is an entity for a non-imported subprogram specification with
+      --  pre/postconditions and we are compiling with CodePeer mode, then this
+      --  procedure will create a wrapper to help Gnat2scil process its
+      --  contracts. Return Empty if the wrapper cannot be built.
+
+      function Build_Contract_Only_Subprograms (L : List_Id) return List_Id;
+      --  Build the contract-only subprograms of all eligible subprograms found
+      --  in list L.
+
+      function Has_Private_Declarations (N : Node_Id) return Boolean;
+      --  Return True for package specs, task definitions, and protected type
+      --  definitions whose list of private declarations is not empty.
+
+      ---------------------------------------
+      -- Analyze_Contract_Only_Subprograms --
+      ---------------------------------------
+
+      procedure Analyze_Contract_Only_Subprograms (L : List_Id) is
+         procedure Analyze_Contract_Only_Bodies;
+         --  Analyze all the contract-only bodies of L
+
+         ----------------------------------
+         -- Analyze_Contract_Only_Bodies --
+         ----------------------------------
+
+         procedure Analyze_Contract_Only_Bodies is
+            Decl : Node_Id;
+
+         begin
+            Decl := First (L);
+            while Present (Decl) loop
+               if Nkind (Decl) = N_Subprogram_Body
+                 and then Is_Contract_Only_Body
+                            (Defining_Unit_Name (Specification (Decl)))
+               then
+                  Analyze (Decl);
+               end if;
+
+               Next (Decl);
+            end loop;
+         end Analyze_Contract_Only_Bodies;
+
+      --  Start of processing for Analyze_Contract_Only_Subprograms
+
+      begin
+         if Ekind (Current_Scope) /= E_Package then
+            Analyze_Contract_Only_Bodies;
+
+         else
+            declare
+               Pkg_Spec : constant Node_Id :=
+                            Package_Specification (Current_Scope);
+
+            begin
+               if not Has_Private_Declarations (Pkg_Spec) then
+                  Analyze_Contract_Only_Bodies;
+
+               --  For packages with private declarations, the contract-only
+               --  bodies of subprograms defined in the visible part of the
+               --  package are added to its private declarations (to ensure
+               --  that they do not cause premature freezing of types and also
+               --  that they are analyzed with proper visibility). Hence they
+               --  will be analyzed later.
+
+               elsif Visible_Declarations (Pkg_Spec) = L then
+                  null;
+
+               elsif Private_Declarations (Pkg_Spec) = L then
+                  Analyze_Contract_Only_Bodies;
+               end if;
+            end;
+         end if;
+      end Analyze_Contract_Only_Subprograms;
+
+      --------------------------------------
+      -- Append_Contract_Only_Subprograms --
+      --------------------------------------
+
+      procedure Append_Contract_Only_Subprograms (Subp_List : List_Id) is
+      begin
+         if No (Subp_List) then
+            return;
+         end if;
+
+         if Ekind (Current_Scope) /= E_Package then
+            Append_List (Subp_List, To => L);
+
+         else
+            declare
+               Pkg_Spec : constant Node_Id :=
+                            Package_Specification (Current_Scope);
+
+            begin
+               if not Has_Private_Declarations (Pkg_Spec) then
+                  Append_List (Subp_List, To => L);
+
+               --  If the package has private declarations then append them to
+               --  its private declarations; they will be analyzed when the
+               --  contracts of its private declarations are analyzed.
+
+               else
+                  Append_List
+                    (List => Subp_List,
+                     To   => Private_Declarations (Pkg_Spec));
+               end if;
+            end;
+         end if;
+      end Append_Contract_Only_Subprograms;
+
+      ------------------------------------
+      -- Build_Contract_Only_Subprogram --
+      ------------------------------------
+
+      --  This procedure takes care of building a wrapper to generate better
+      --  analysis results in the case of a call to a subprogram whose body
+      --  is unavailable to CodePeer but whose specification includes Pre/Post
+      --  conditions. The body might be unavailable for any of a number or
+      --  reasons (it is imported, the .adb file is simply missing, or the
+      --  subprogram might be subject to an Annotate (CodePeer, Skip_Analysis)
+      --  pragma). The built subprogram has the following contents:
+      --    * check preconditions
+      --    * call the subprogram
+      --    * check postconditions
+
+      function Build_Contract_Only_Subprogram (E : Entity_Id) return Node_Id is
+         Loc : constant Source_Ptr := Sloc (E);
+
+         function Build_Missing_Body_Decls return List_Id;
+         --  Build the declaration of the missing body subprogram and its
+         --  corresponding pragma Import.
+
+         function Build_Missing_Body_Subprogram_Call return Node_Id;
+         --  Build the call to the missing body subprogram
+
+         function Copy_Original_Specification
+           (Loc  : Source_Ptr;
+            Spec : Node_Id) return Node_Id;
+         --  Build a copy of the original specification of the given subprogram
+         --  specification.
+
+         function Skip_Contract_Only_Subprogram (E : Entity_Id) return Boolean;
+         --  Return True if E is a subprogram declared in a nested package that
+         --  has some formal or return type depending on a private type defined
+         --  in an enclosing package.
+
+         ------------------------------
+         -- Build_Missing_Body_Decls --
+         ------------------------------
+
+         function Build_Missing_Body_Decls return List_Id is
+            Name : constant Name_Id := Get_Contract_Only_Missing_Body_Name (E);
+            Spec : constant Node_Id := Declaration_Node (E);
+            Decl : Node_Id;
+            Prag : Node_Id;
+
+         begin
+            Decl := Make_Subprogram_Declaration (Loc,
+                      Copy_Original_Specification (Loc, Spec));
+            Set_Chars (Defining_Unit_Name (Specification (Decl)), Name);
+
+            Prag :=
+              Make_Pragma (Loc,
+                Chars => Name_Import,
+                Pragma_Argument_Associations => New_List (
+                  Make_Pragma_Argument_Association (Loc,
+                    Expression => Make_Identifier (Loc, Name_Ada)),
+
+                  Make_Pragma_Argument_Association (Loc,
+                    Expression => Make_Identifier (Loc, Name))));
+
+            return New_List (Decl, Prag);
+         end Build_Missing_Body_Decls;
+
+         ----------------------------------------
+         -- Build_Missing_Body_Subprogram_Call --
+         ----------------------------------------
+
+         function Build_Missing_Body_Subprogram_Call return Node_Id is
+            Forml : Entity_Id;
+            Parms : List_Id;
+
+         begin
+            --  Build parameter list that we need
+
+            Parms := New_List;
+            Forml := First_Formal (E);
+            while Present (Forml) loop
+               Append_To (Parms, Make_Identifier (Loc, Chars (Forml)));
+               Next_Formal (Forml);
+            end loop;
+
+            --  Build the call to the missing body subprogram
+
+            if Ekind_In (E, E_Function, E_Generic_Function) then
+               return
+                 Make_Simple_Return_Statement (Loc,
+                   Expression =>
+                     Make_Function_Call (Loc,
+                       Name => Make_Identifier (Loc,
+                                 Get_Contract_Only_Missing_Body_Name (E)),
+                       Parameter_Associations => Parms));
+
+            else
+               return
+                 Make_Procedure_Call_Statement (Loc,
+                   Name => Make_Identifier (Loc,
+                             Get_Contract_Only_Missing_Body_Name (E)),
+                   Parameter_Associations => Parms);
+            end if;
+         end Build_Missing_Body_Subprogram_Call;
+
+         ---------------------------------
+         -- Copy_Original_Specification --
+         ---------------------------------
+
+         function Copy_Original_Specification
+           (Loc  : Source_Ptr;
+            Spec : Node_Id) return Node_Id
+         is
+            function Copy_Original_Type (N : Node_Id) return Node_Id;
+            --  Duplicate the original type of a given formal or function
+            --  result type.
+
+            function Copy_Original_Type (N : Node_Id) return Node_Id is
+            begin
+               --  For expanded names located in instantiations, copy them with
+               --  semantic information (avoids visibility problems).
+
+               if In_Instance
+                 and then Nkind (N) = N_Expanded_Name
+               then
+                  return New_Copy_Tree (N);
+               else
+                  return Copy_Separate_Tree (Original_Node (N));
+               end if;
+            end Copy_Original_Type;
+
+            --  Local variables
+
+            Current_Parameter  : Node_Id;
+            Current_Identifier : Entity_Id;
+            Current_Type       : Node_Id;
+            New_Identifier     : Entity_Id;
+            Parameters         : List_Id := No_List;
+
+         --  Start of processing for Copy_Original_Specification
+
+         begin
+            if Present (Parameter_Specifications (Spec)) then
+               Parameters        := New_List;
+               Current_Parameter := First (Parameter_Specifications (Spec));
+               while Present (Current_Parameter) loop
+                  Current_Identifier :=
+                    Defining_Identifier (Current_Parameter);
+                  Current_Type :=
+                    Copy_Original_Type (Parameter_Type (Current_Parameter));
+
+                  New_Identifier := Make_Defining_Identifier (Loc,
+                    Chars (Current_Identifier));
+
+                  Append_To (Parameters,
+                    Make_Parameter_Specification (Loc,
+                      Defining_Identifier => New_Identifier,
+                      Parameter_Type      => Current_Type,
+                      In_Present          => In_Present (Current_Parameter),
+                      Out_Present         => Out_Present (Current_Parameter),
+                      Expression          =>
+                        Copy_Separate_Tree (Expression (Current_Parameter))));
+
+                  Next (Current_Parameter);
+               end loop;
+            end if;
+
+            case Nkind (Spec) is
+
+               when N_Function_Specification =>
+                  return
+                    Make_Function_Specification (Loc,
+                      Defining_Unit_Name       =>
+                        Make_Defining_Identifier (Loc,
+                          Chars => Chars (Defining_Unit_Name (Spec))),
+                      Parameter_Specifications => Parameters,
+                      Result_Definition        =>
+                        Copy_Original_Type (Result_Definition (Spec)));
+
+               when N_Procedure_Specification =>
+                  return
+                    Make_Procedure_Specification (Loc,
+                      Defining_Unit_Name       =>
+                        Make_Defining_Identifier (Loc,
+                          Chars => Chars (Defining_Unit_Name (Spec))),
+                      Parameter_Specifications => Parameters);
+
+               when others =>
+                  raise Program_Error;
+            end case;
+         end Copy_Original_Specification;
+
+         -----------------------------------
+         -- Skip_Contract_Only_Subprogram --
+         -----------------------------------
+
+         function Skip_Contract_Only_Subprogram (E : Entity_Id) return Boolean
+         is
+            function Depends_On_Enclosing_Private_Type return Boolean;
+            --  Return True if some formal of E (or its return type) are
+            --  private types defined in an enclosing package.
+
+            function Some_Enclosing_Package_Has_Private_Decls return Boolean;
+            --  Return True if some enclosing package of the current scope has
+            --  private declarations.
+
+            ---------------------------------------
+            -- Depends_On_Enclosing_Private_Type --
+            ---------------------------------------
+
+            function Depends_On_Enclosing_Private_Type return Boolean is
+
+               function Defined_In_Enclosing_Package
+                  (Typ : Entity_Id) return Boolean;
+               --  Return True if Typ is an entity defined in an enclosing
+               --  package of the current scope.
+
+               ----------------------------------
+               -- Defined_In_Enclosing_Package --
+               ----------------------------------
+
+               function Defined_In_Enclosing_Package
+                  (Typ : Entity_Id) return Boolean
+               is
+                  Scop : Entity_Id := Scope (Current_Scope);
+
+               begin
+                  while Scop /= Scope (Typ)
+                     and then not Is_Compilation_Unit (Scop)
+                  loop
+                     Scop := Scope (Scop);
+                  end loop;
+
+                  return Scop = Scope (Typ);
+               end Defined_In_Enclosing_Package;
+
+               --  Local variables
+
+               Param_E : Entity_Id;
+               Typ     : Entity_Id;
+            begin
+               Param_E := First_Entity (E);
+               while Present (Param_E) loop
+                  Typ := Etype (Param_E);
+
+                  if Is_Private_Type (Typ)
+                    and then Defined_In_Enclosing_Package (Typ)
+                  then
+                     return True;
+                  end if;
+
+                  Next_Entity (Param_E);
+               end loop;
+
+               return Ekind (E) = E_Function
+                 and then Is_Private_Type (Etype (E))
+                 and then Defined_In_Enclosing_Package (Etype (E));
+            end Depends_On_Enclosing_Private_Type;
+
+            ----------------------------------------------
+            -- Some_Enclosing_Package_Has_Private_Decls --
+            ----------------------------------------------
+
+            function Some_Enclosing_Package_Has_Private_Decls return Boolean is
+               Scop     : Entity_Id := Current_Scope;
+               Pkg_Spec : Node_Id   := Package_Specification (Scop);
+
+            begin
+               loop
+                  if Ekind (Scop) = E_Package
+                    and then
+                      Has_Private_Declarations (Package_Specification (Scop))
+                  then
+                     Pkg_Spec := Package_Specification (Scop);
+                  end if;
+
+                  exit when Is_Compilation_Unit (Scop);
+                  Scop := Scope (Scop);
+               end loop;
+
+               return Pkg_Spec /= Package_Specification (Current_Scope);
+            end Some_Enclosing_Package_Has_Private_Decls;
+
+         --  Start of processing for Skip_Contract_Only_Subprogram
+
+         begin
+            if Ekind (Current_Scope) = E_Package
+              and then Some_Enclosing_Package_Has_Private_Decls
+              and then Depends_On_Enclosing_Private_Type
+            then
+               if Debug_Flag_Dot_KK then
+                  declare
+                     Saved_Mode : constant Warning_Mode_Type := Warning_Mode;
+
+                  begin
+                     --  Warnings are disabled by default under CodePeer_Mode
+                     --  (see switch-c). Enable them temporarily.
+
+                     Warning_Mode := Normal;
+                     Error_Msg_N
+                       ("cannot generate contract-only subprogram?", E);
+                     Warning_Mode := Saved_Mode;
+                  end;
+               end if;
+
+               return True;
+            end if;
+
+            return False;
+         end Skip_Contract_Only_Subprogram;
+
+      --  Start of processing for Build_Contract_Only_Subprogram
+
+      begin
+         --  Test cases where the wrapper is not needed and cases where we
+         --  cannot build the wrapper.
+
+         if not CodePeer_Mode
+           or else Inside_A_Generic
+           or else not Is_Subprogram (E)
+           or else Is_Abstract_Subprogram (E)
+           or else Is_Imported (E)
+           or else No (Contract (E))
+           or else No (Pre_Post_Conditions (Contract (E)))
+           or else Is_Contract_Only_Body (E)
+           or else Skip_Contract_Only_Subprogram (E)
+           or else Convention (E) = Convention_Protected
+         then
+            return Empty;
+         end if;
+
+         --  Note on calls to Copy_Separate_Tree. The trees we are copying
+         --  here are fully analyzed, but we definitely want fully syntactic
+         --  unanalyzed trees in the body we construct, so that the analysis
+         --  generates the right visibility, and that is exactly what the
+         --  calls to Copy_Separate_Tree give us.
+
+         declare
+            Name : constant Name_Id := Get_Contract_Only_Body_Name (E);
+            Id   : Entity_Id;
+            Bod  : Node_Id;
+
+         begin
+            Bod :=
+              Make_Subprogram_Body (Loc,
+                Specification              =>
+                  Copy_Original_Specification (Loc, Declaration_Node (E)),
+                Declarations               =>
+                  Build_Missing_Body_Decls,
+                Handled_Statement_Sequence =>
+                  Make_Handled_Sequence_Of_Statements (Loc,
+                    Statements => New_List (
+                                    Build_Missing_Body_Subprogram_Call),
+                    End_Label  => Make_Identifier (Loc, Name)));
+
+            Id := Defining_Unit_Name (Specification (Bod));
+
+            --  Copy only the pre/postconditions of the original contract
+            --  since it is what we need, but also because pragmas stored in
+            --  the other fields have N_Pragmas with N_Aspect_Specifications
+            --  that reference their associated pragma (thus causing an endless
+            --  loop when trying to copy the subtree).
+
+            declare
+               New_Contract : constant Node_Id := Make_Contract (Sloc (E));
+
+            begin
+               Set_Pre_Post_Conditions (New_Contract,
+                 Copy_Separate_Tree (Pre_Post_Conditions (Contract (E))));
+               Set_Contract (Id, New_Contract);
+            end;
+
+            --  Fix the name of this new subprogram and link the original
+            --  subprogram with its Contract_Only_Body subprogram.
+
+            Set_Chars (Id, Name);
+            Set_Is_Contract_Only_Body (Id);
+            Set_Contract_Only_Body (E, Id);
+
+            return Bod;
+         end;
+      end Build_Contract_Only_Subprogram;
+
+      -------------------------------------
+      -- Build_Contract_Only_Subprograms --
+      -------------------------------------
+
+      function Build_Contract_Only_Subprograms (L : List_Id) return List_Id is
+         Decl     : Node_Id;
+         Subp_Id  : Entity_Id;
+         New_Subp : Node_Id;
+         Result   : List_Id := No_List;
+
+      begin
+         Decl := First (L);
+         while Present (Decl) loop
+            if Nkind (Decl) = N_Subprogram_Declaration then
+               Subp_Id  := Defining_Unit_Name (Specification (Decl));
+               New_Subp := Build_Contract_Only_Subprogram (Subp_Id);
+
+               if Present (New_Subp) then
+                  if No (Result) then
+                     Result := New_List;
+                  end if;
+
+                  Append_To (Result, New_Subp);
+               end if;
+            end if;
+
+            Next (Decl);
+         end loop;
+
+         return Result;
+      end Build_Contract_Only_Subprograms;
+
+      ------------------------------
+      -- Has_Private_Declarations --
+      ------------------------------
+
+      function Has_Private_Declarations (N : Node_Id) return Boolean is
+      begin
+         if not Nkind_In (N, N_Package_Specification,
+                             N_Task_Definition,
+                             N_Protected_Definition)
+         then
+            return False;
+         else
+            return Present (Private_Declarations (N))
+               and then Is_Non_Empty_List (Private_Declarations (N));
+         end if;
+      end Has_Private_Declarations;
+
+      --  Local variables
+
+      Subp_List : List_Id;
+
+   --  Start of processing for Build_And_Analyze_Contract_Only_Subprograms
+
+   begin
+      Subp_List := Build_Contract_Only_Subprograms (L);
+      Append_Contract_Only_Subprograms (Subp_List);
+      Analyze_Contract_Only_Subprograms (L);
+   end Build_And_Analyze_Contract_Only_Subprograms;
+
 end Contracts;
diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb
index e3c53dd..a045a7b 100644
--- a/gcc/ada/debug.adb
+++ b/gcc/ada/debug.adb
@@ -128,7 +128,7 @@ package body Debug is
    --  d.H  GNSA mode for ASIS
    --  d.I  Do not ignore enum representation clauses in CodePeer mode
    --  d.J  Disable parallel SCIL generation mode
-   --  d.K
+   --  d.K  Enable generation of contract-only procedures in CodePeer mode
    --  d.L  Depend on back end for limited types in if and case expressions
    --  d.M  Relaxed RM semantics
    --  d.N  Add node to all entities
@@ -646,6 +646,13 @@ package body Debug is
    --       done in parallel to speed processing. This switch disables this
    --       behavior.
 
+   --  d.K  Enable generation of contract-only procedures in CodePeer mode and
+   --       report a warning on subprograms for which the contract-only body
+   --       cannot be built. Currently reported on subprograms defined in
+   --       nested package specs that have some formal (or return type) whose
+   --       type is a private type defined in some enclosing package and that
+   --       have pre/postconditions.
+
    --  d.L  Normally the front end generates special expansion for conditional
    --       expressions of a limited type. This debug flag removes this special
    --       case expansion, leaving it up to the back end to handle conditional
diff --git a/gcc/ada/exp_attr.adb b/gcc/ada/exp_attr.adb
index 57905df..074a5b1 100644
--- a/gcc/ada/exp_attr.adb
+++ b/gcc/ada/exp_attr.adb
@@ -3244,7 +3244,11 @@ package body Exp_Attr is
             Rewrite (N, Make_Integer_Literal (Loc, 0));
          end if;
 
-         Analyze (N);
+         --  Due to cases where the entity type of the attribute is already
+         --  resolved the rewritten N must get re-resolved to its appropriate
+         --  type.
+
+         Analyze_And_Resolve (N, Typ);
       end Finalization_Size;
 
       -----------
diff --git a/gcc/ada/exp_ch5.adb b/gcc/ada/exp_ch5.adb
index dff953b..ed3703a 100644
--- a/gcc/ada/exp_ch5.adb
+++ b/gcc/ada/exp_ch5.adb
@@ -2939,7 +2939,7 @@ package body Exp_Ch5 is
       --  For an element iterator, the Element aspect must be present,
       --  (this is checked during analysis) and the expansion takes the form:
 
-      --    Cursor : Cursor_type := First (Container);
+      --    Cursor : Cursor_Type := First (Container);
       --    Elmt : Element_Type;
       --    while Has_Element (Cursor, Container) loop
       --       Elmt := Element (Container, Cursor);
@@ -2951,10 +2951,10 @@ package body Exp_Ch5 is
       --   In that case we create a block to hold a variable declaration
       --   initialized with a call to Element, and generate:
 
-      --    Cursor : Cursor_type := First (Container);
+      --    Cursor : Cursor_Type := First (Container);
       --    while Has_Element (Cursor, Container) loop
       --       declare
-      --          Elmt : Element-Type := Element (Container, Cursor);
+      --          Elmt : Element_Type := Element (Container, Cursor);
       --       begin
       --          <original loop statements>
       --          Cursor := Next (Container, Cursor);
@@ -2968,7 +2968,7 @@ package body Exp_Ch5 is
       Set_Ekind (Cursor, E_Variable);
       Insert_Action (N, Init);
 
-      --  Declaration for Element.
+      --  Declaration for Element
 
       Elmt_Decl :=
         Make_Object_Declaration (Loc,
diff --git a/gcc/ada/exp_ch6.adb b/gcc/ada/exp_ch6.adb
index 145ae93..7b7e135 100644
--- a/gcc/ada/exp_ch6.adb
+++ b/gcc/ada/exp_ch6.adb
@@ -2264,7 +2264,9 @@ package body Exp_Ch6 is
       --  expression for the value of the actual, EF is the entity for the
       --  extra formal.
 
-      procedure Check_View_Conversion (Formal : Entity_Id; Actual : Node_Id);
+      procedure Add_View_Conversion_Invariants
+        (Formal : Entity_Id;
+         Actual : Node_Id);
       --  Adds invariant checks for every intermediate type between the range
       --  of a view converted argument to its ancestor (from parent to child).
 
@@ -2354,11 +2356,14 @@ package body Exp_Ch6 is
          end if;
       end Add_Extra_Actual;
 
-      ---------------------------
-      -- Check_View_Conversion --
-      ---------------------------
+      ------------------------------------
+      -- Add_View_Conversion_Invariants --
+      ------------------------------------
 
-      procedure Check_View_Conversion (Formal : Entity_Id; Actual : Node_Id) is
+      procedure Add_View_Conversion_Invariants
+        (Formal : Entity_Id;
+         Actual : Node_Id)
+      is
          Arg        : Entity_Id;
          Curr_Typ   : Entity_Id;
          Inv_Checks : List_Id;
@@ -2407,7 +2412,7 @@ package body Exp_Ch6 is
          if not Is_Empty_List (Inv_Checks) then
             Insert_Actions_After (N, Inv_Checks);
          end if;
-      end Check_View_Conversion;
+      end Add_View_Conversion_Invariants;
 
       ---------------------------
       -- Inherited_From_Formal --
@@ -3292,15 +3297,18 @@ package body Exp_Ch6 is
                 Duplicate_Subexpr_Move_Checks (Actual)));
          end if;
 
-         --  Invariant checks are performed for every intermediate type between
-         --  the range of a view converted argument to its ancestor (from
-         --  parent to child) if it is passed as an "out" or "in out" parameter
-         --  after executing the call (RM 7.3.2 (12/3, 13/3, 14/3)).
+         --  Perform invariant checks for all intermediate types in a view
+         --  conversion after successful return from a call that passes the
+         --  view conversion as an IN OUT or OUT parameter (RM 7.3.2 (12/3,
+         --  13/3, 14/3)). Consider only source conversion in order to avoid
+         --  generating spurious checks on complex expansion such as object
+         --  initialization through an extension aggregate.
 
-         if Ekind (Formal) /= E_In_Parameter
+         if Comes_From_Source (N)
+           and then Ekind (Formal) /= E_In_Parameter
            and then Nkind (Actual) = N_Type_Conversion
          then
-            Check_View_Conversion (Formal, Actual);
+            Add_View_Conversion_Invariants (Formal, Actual);
          end if;
 
          --  This label is required when skipping extra actual generation for
diff --git a/gcc/ada/exp_sel.ads b/gcc/ada/exp_sel.ads
index 440a0ea..0ba7669 100644
--- a/gcc/ada/exp_sel.ads
+++ b/gcc/ada/exp_sel.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1992-2011, 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- --
@@ -48,7 +48,7 @@ package Exp_Sel is
    function Build_Abort_Block_Handler (Loc : Source_Ptr) return Node_Id;
    --  Generate if front-end exception:
    --    when others =>
-   --      Abort_Under;
+   --      Abort_Undefer;
    --  or if back-end exception:
    --    when others =>
    --      null;
diff --git a/gcc/ada/exp_spark.adb b/gcc/ada/exp_spark.adb
index 6ac38d6..a0721f6 100644
--- a/gcc/ada/exp_spark.adb
+++ b/gcc/ada/exp_spark.adb
@@ -140,7 +140,7 @@ package body Exp_SPARK is
             --  Otherwise the renamed object denotes a name
 
             else
-               Rewrite (N, New_Copy_Tree (Obj_Id));
+               Rewrite (N, New_Copy_Tree (Obj_Id, New_Sloc => Loc));
                Reset_Analyzed_Flags (N);
             end if;
 
diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
index 7791ad46..f19b6e3 100644
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -1897,13 +1897,19 @@ package body Exp_Util is
       Set_Corresponding_Spec (Proc_Body, Proc_Id);
 
       --  The body should not be inserted into the tree when the context is
-      --  ASIS, GNATprove or a generic unit because it is not part of the
-      --  template. Note that the body must still be generated in order to
-      --  resolve the DIC assertion expression.
+      --  ASIS or a generic unit because it is not part of the template. Note
+      --  that the body must still be generated in order to resolve the DIC
+      --  assertion expression.
 
-      if ASIS_Mode or GNATprove_Mode or Inside_A_Generic then
+      if ASIS_Mode or Inside_A_Generic then
          null;
 
+      --  Semi-insert the body into the tree for GNATprove by setting its
+      --  Parent field. This allows for proper upstream tree traversals.
+
+      elsif GNATprove_Mode then
+         Set_Parent (Proc_Body, Parent (Declaration_Node (Work_Typ)));
+
       --  Otherwise the body is part of the freezing actions of the working
       --  type.
 
@@ -2083,16 +2089,20 @@ package body Exp_Util is
                     New_Occurrence_Of (Work_Typ, Loc)))));
 
       --  The declaration should not be inserted into the tree when the context
-      --  is ASIS, GNATprove, or a generic unit because it is not part of the
-      --  template.
+      --  is ASIS or a generic unit because it is not part of the template.
 
-      if ASIS_Mode or GNATprove_Mode or Inside_A_Generic then
+      if ASIS_Mode or Inside_A_Generic then
          null;
 
+      --  Semi-insert the declaration into the tree for GNATprove by setting
+      --  its Parent field. This allows for proper upstream tree traversals.
+
+      elsif GNATprove_Mode then
+         Set_Parent (Proc_Decl, Parent (Typ_Decl));
+
       --  Otherwise insert the declaration
 
       else
-         pragma Assert (Present (Typ_Decl));
          Insert_After_And_Analyze (Typ_Decl, Proc_Decl);
       end if;
 
diff --git a/gcc/ada/lib-writ.ads b/gcc/ada/lib-writ.ads
index b38003b..0060c9e 100644
--- a/gcc/ada/lib-writ.ads
+++ b/gcc/ada/lib-writ.ads
@@ -649,10 +649,8 @@ package Lib.Writ is
    --        AD  Elaborate_All_Desirable set for this unit, which means that
    --            there is no Elaborate_All, but the analysis suggests that
    --            Program_Error may be raised if the Elaborate_All conditions
-   --            cannot be satisfied. In dynamic elaboration mode, the binder
-   --            will attempt to treat AD as EA if it can. In static
-   --            elaboration mode, the binder will treat AD as EA, even if it
-   --            introduces cycles.
+   --            cannot be satisfied. The binder will attempt to treat AD as
+   --            EA if it can.
 
    --      The parameter source-name and lib-name are omitted for the case of a
    --      generic unit compiled with earlier versions of GNAT which did not
diff --git a/gcc/ada/scil_ll.adb b/gcc/ada/scil_ll.adb
index 470ac98..eed0d1a 100644
--- a/gcc/ada/scil_ll.adb
+++ b/gcc/ada/scil_ll.adb
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 2010-2012, Free Software Foundation, Inc.         --
+--          Copyright (C) 2010-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- --
@@ -29,63 +29,105 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
-with Alloc; use Alloc;
-with Atree; use Atree;
-with Opt;   use Opt;
-with Sinfo; use Sinfo;
-with Table;
+with Atree;         use Atree;
+with Opt;           use Opt;
+with Sinfo;         use Sinfo;
+with System.HTable; use System.HTable;
 
 package body SCIL_LL is
+   Contract_Only_Body_Suffix : constant String := "__contract_only";
+   --  Suffix of Contract_Only_Body subprograms internally built only under
+   --  CodePeer mode
+
+   Contract_Only_Missing_Body_Suffix : constant String := "__missing_body";
+   --  Suffix of Contract_Only_Missing_Body subprograms internally built only
+   --  under CodePeer mode
 
    procedure Copy_SCIL_Node (Target : Node_Id; Source : Node_Id);
    --  Copy the SCIL field from Source to Target (it is used as the argument
    --  for a call to Set_Reporting_Proc in package atree).
 
-   function SCIL_Nodes_Table_Size return Pos;
-   --  Used to initialize the table of SCIL nodes because we do not want
-   --  to consume memory for this table if it is not required.
+   type Header_Num is range 1 .. 4096;
+
+   function Hash (N : Node_Id) return Header_Num;
+   --  Hash function for Node_Ids
+
+   --------------------------
+   -- Internal Hash Tables --
+   --------------------------
+
+   package Contract_Only_Body_Flag is new Simple_HTable
+     (Header_Num => Header_Num,
+      Element    => Boolean,
+      No_Element => False,
+      Key        => Node_Id,
+      Hash       => Hash,
+      Equal      => "=");
+   --  This table records the value of flag Is_Contract_Only_Flag of tree nodes
+
+   package Contract_Only_Body_Nodes is new Simple_HTable
+     (Header_Num => Header_Num,
+      Element    => Node_Id,
+      No_Element => Empty,
+      Key        => Node_Id,
+      Hash       => Hash,
+      Equal      => "=");
+   --  This table records the value of attribute Contract_Only_Body of tree
+   --  nodes.
+
+   package SCIL_Nodes is new Simple_HTable
+     (Header_Num => Header_Num,
+      Element    => Node_Id,
+      No_Element => Empty,
+      Key        => Node_Id,
+      Hash       => Hash,
+      Equal      => "=");
+   --  This table records the value of attribute SCIL_Node of tree nodes.
+
+   --------------------
+   -- Copy_SCIL_Node --
+   --------------------
+
+   procedure Copy_SCIL_Node (Target : Node_Id; Source : Node_Id) is
+   begin
+      Set_SCIL_Node (Target, Get_SCIL_Node (Source));
+   end Copy_SCIL_Node;
 
    ----------------------------
-   --  SCIL_Nodes_Table_Size --
+   -- Get_Contract_Only_Body --
    ----------------------------
 
-   function SCIL_Nodes_Table_Size return Pos is
+   function Get_Contract_Only_Body (N : Node_Id) return Node_Id is
    begin
-      if Generate_SCIL then
-         return Alloc.Orig_Nodes_Initial;
+      if CodePeer_Mode
+        and then Present (N)
+      then
+         return Contract_Only_Body_Nodes.Get (N);
       else
-         return 1;
+         return Empty;
       end if;
-   end SCIL_Nodes_Table_Size;
-
-   package SCIL_Nodes is new Table.Table (
-      Table_Component_Type => Node_Id,
-      Table_Index_Type     => Node_Id'Base,
-      Table_Low_Bound      => First_Node_Id,
-      Table_Initial        => SCIL_Nodes_Table_Size,
-      Table_Increment      => Alloc.Orig_Nodes_Increment,
-      Table_Name           => "SCIL_Nodes");
-   --  This table records the value of attribute SCIL_Node of all the
-   --  tree nodes.
+   end Get_Contract_Only_Body;
 
-   --------------------
-   -- Copy_SCIL_Node --
-   --------------------
+   ---------------------------------
+   -- Get_Contract_Only_Body_Name --
+   ---------------------------------
 
-   procedure Copy_SCIL_Node (Target : Node_Id; Source : Node_Id) is
+   function Get_Contract_Only_Body_Name (E : Entity_Id) return Name_Id is
    begin
-      Set_SCIL_Node (Target, Get_SCIL_Node (Source));
-   end Copy_SCIL_Node;
+      return Name_Find (Get_Name_String (Chars (E)) &
+                          Contract_Only_Body_Suffix);
+   end Get_Contract_Only_Body_Name;
 
-   ----------------
-   -- Initialize --
-   ----------------
+   -----------------------------------------
+   -- Get_Contract_Only_Missing_Body_Name --
+   -----------------------------------------
 
-   procedure Initialize is
+   function Get_Contract_Only_Missing_Body_Name (E : Entity_Id)
+      return Name_Id is
    begin
-      SCIL_Nodes.Init;
-      Set_Reporting_Proc (Copy_SCIL_Node'Access);
-   end Initialize;
+      return Name_Find (Get_Name_String (Chars (E)) &
+                          Contract_Only_Missing_Body_Suffix);
+   end Get_Contract_Only_Missing_Body_Name;
 
    -------------------
    -- Get_SCIL_Node --
@@ -96,12 +138,64 @@ package body SCIL_LL is
       if Generate_SCIL
         and then Present (N)
       then
-         return SCIL_Nodes.Table (N);
+         return SCIL_Nodes.Get (N);
       else
          return Empty;
       end if;
    end Get_SCIL_Node;
 
+   ----------
+   -- Hash --
+   ----------
+
+   function Hash (N : Node_Id) return Header_Num is
+   begin
+      return Header_Num (1 + N mod Node_Id (Header_Num'Last));
+   end Hash;
+
+   ----------------
+   -- Initialize --
+   ----------------
+
+   procedure Initialize is
+   begin
+      SCIL_Nodes.Reset;
+      Contract_Only_Body_Nodes.Reset;
+      Contract_Only_Body_Flag.Reset;
+      Set_Reporting_Proc (Copy_SCIL_Node'Access);
+   end Initialize;
+
+   ---------------------------
+   -- Is_Contract_Only_Body --
+   ---------------------------
+
+   function Is_Contract_Only_Body (E : Entity_Id) return Boolean is
+   begin
+      return Contract_Only_Body_Flag.Get (E);
+   end Is_Contract_Only_Body;
+
+   ----------------------------
+   -- Set_Contract_Only_Body --
+   ----------------------------
+
+   procedure Set_Contract_Only_Body (N : Node_Id; Value : Node_Id) is
+   begin
+      pragma Assert (CodePeer_Mode
+        and then Present (N)
+        and then Is_Contract_Only_Body (Value));
+
+      Contract_Only_Body_Nodes.Set (N, Value);
+   end Set_Contract_Only_Body;
+
+   -------------------------------
+   -- Set_Is_Contract_Only_Body --
+   -------------------------------
+
+   procedure Set_Is_Contract_Only_Body (E : Entity_Id) is
+   begin
+      Contract_Only_Body_Flag.Set (E, True);
+   end Set_Is_Contract_Only_Body;
+
    -------------------
    -- Set_SCIL_Node --
    -------------------
@@ -133,11 +227,7 @@ package body SCIL_LL is
          end case;
       end if;
 
-      if Atree.Last_Node_Id > SCIL_Nodes.Last then
-         SCIL_Nodes.Set_Last (Atree.Last_Node_Id);
-      end if;
-
-      SCIL_Nodes.Set_Item (N, Value);
+      SCIL_Nodes.Set (N, Value);
    end Set_SCIL_Node;
 
 end SCIL_LL;
diff --git a/gcc/ada/scil_ll.ads b/gcc/ada/scil_ll.ads
index 8265a19..bfac1a0 100644
--- a/gcc/ada/scil_ll.ads
+++ b/gcc/ada/scil_ll.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---             Copyright (C) 2010, Free Software Foundation, Inc.           --
+--          Copyright (C) 2010-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- --
@@ -29,20 +29,39 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
---  This package extends the tree nodes with a field that is used to reference
---  the SCIL node.
+--  This package extends the tree nodes with fields that are used to reference
+--  the SCIL node and the Contract_Only_Body of a subprogram with aspects.
 
+with Namet; use Namet;
 with Types; use Types;
 
 package SCIL_LL is
 
+   function Get_Contract_Only_Body_Name (E : Entity_Id) return Name_Id;
+   --  Return the name of the Contract_Only_Body subprogram of E
+
+   function Get_Contract_Only_Missing_Body_Name (E : Entity_Id) return Name_Id;
+   --  Return the name of the Contract_Only_Missing_Body subprogram of E
+
+   function Get_Contract_Only_Body (N : Node_Id) return Node_Id;
+   --  Read the value of attribute Contract_Only_Body
+
    function Get_SCIL_Node (N : Node_Id) return Node_Id;
    --  Read the value of attribute SCIL node
 
+   procedure Set_Contract_Only_Body (N : Node_Id; Value : Node_Id);
+   --  Set the value of attribute Contract_Only_Body
+
    procedure Set_SCIL_Node (N : Node_Id; Value : Node_Id);
    --  Set the value of attribute SCIL node
 
    procedure Initialize;
    --  Initialize the table of SCIL nodes
 
+   function Is_Contract_Only_Body (E : Entity_Id) return Boolean;
+   --  Return True if E is a Contract_Only_Body subprogram
+
+   procedure Set_Is_Contract_Only_Body (E : Entity_Id);
+   --  Set E as Contract_Only_Body subprogram
+
 end SCIL_LL;
diff --git a/gcc/ada/sem.ads b/gcc/ada/sem.ads
index 9adc8b2..6cd050e 100644
--- a/gcc/ada/sem.ads
+++ b/gcc/ada/sem.ads
@@ -523,8 +523,8 @@ package Sem is
       --  See Sem_Ch10 (Install_Parents, Remove_Parents).
 
       Node_To_Be_Wrapped : Node_Id;
-      --  Only used in transient scopes. Records the node which will
-      --  be wrapped by the transient block.
+      --  Only used in transient scopes. Records the node which will be wrapped
+      --  by the transient block.
 
       Actions_To_Be_Wrapped : Scope_Actions;
       --  Actions that have to be inserted at the start, at the end, or as
diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
index c8ca67c..1c5fe4c 100644
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -11810,8 +11810,7 @@ package body Sem_Res is
       -- Valid_Array_Conversion --
       ----------------------------
 
-      function Valid_Array_Conversion return Boolean
-      is
+      function Valid_Array_Conversion return Boolean is
          Opnd_Comp_Type : constant Entity_Id := Component_Type (Opnd_Type);
          Opnd_Comp_Base : constant Entity_Id := Base_Type (Opnd_Comp_Type);
 
diff --git a/gcc/ada/sem_type.adb b/gcc/ada/sem_type.adb
index 3bc27db..555184a 100644
--- a/gcc/ada/sem_type.adb
+++ b/gcc/ada/sem_type.adb
@@ -307,7 +307,6 @@ package body Sem_Type is
             else
                Get_Next_Interp (I, It);
             end if;
-
          end loop;
 
          All_Interp.Table (All_Interp.Last) := (Name, Typ, Abstr_Op);