[multiple changes]

2017-01-13  Gary Dismukes  <dismukes@adacore.com>

	* checks.adb: Minor typo fix and reformatting.

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

	* contracts.adb (Contract_Only_Subprograms): Remove formal.
	(Copy_Original_Specification): Removed.
	(Skip_Contract_Only_Subprogram): Move here checks previously
	located in the caller of this routine (to leave the code more clean).
	(Build_Contract_Only_Subprogram): Code cleanup.
	* scil_ll.ads, scil_ll.adb (Get_Contract_Only_Body_Name): Removed.
	(Get_Contract_Only_Missing_Body_Name): Removed.

From-SVN: r244424

5 files changed, 515 insertions, 612 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 0702a6d..5aa3877 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,17 @@
+2017-01-13  Gary Dismukes  <dismukes@adacore.com>
+
+	* checks.adb: Minor typo fix and reformatting.
+
+2017-01-13  Javier Miranda  <miranda@adacore.com>
+
+	* contracts.adb (Contract_Only_Subprograms): Remove formal.
+	(Copy_Original_Specification): Removed.
+	(Skip_Contract_Only_Subprogram): Move here checks previously
+	located in the caller of this routine (to leave the code more clean).
+	(Build_Contract_Only_Subprogram): Code cleanup.
+	* scil_ll.ads, scil_ll.adb (Get_Contract_Only_Body_Name): Removed.
+	(Get_Contract_Only_Missing_Body_Name): Removed.
+
 2017-01-13  Javier Miranda  <miranda@adacore.com>
 
 	* sem_ch6.adb (Cloned_Expression): New subprogram.
diff --git a/gcc/ada/checks.adb b/gcc/ada/checks.adb
index f67c44f..80b4b4b 100644
--- a/gcc/ada/checks.adb
+++ b/gcc/ada/checks.adb
@@ -3390,10 +3390,10 @@ package body Checks is
                 In_Subrange_Of (Expr_Type, Target_Base, Fixed_Int => Conv_OK)
               and then not Float_To_Int
             then
-               --  A small optimization : the attribute 'Pos applied to an
+               --  A small optimization: the attribute 'Pos applied to an
                --  enumeration type has a known range, even though its type
-               --  is Universal_Integer. so in numeric conversions it is
-               --  usually within range of of the target integer type. Use the
+               --  is Universal_Integer. So in numeric conversions it is
+               --  usually within range of the target integer type. Use the
                --  static bounds of the base types to check.
 
                if Nkind (Expr) = N_Attribute_Reference
@@ -3402,15 +3402,15 @@ package body Checks is
                  and then Is_Integer_Type (Target_Type)
                then
                   declare
-                     Enum_T  : constant Entity_Id :=
-                               Root_Type (Etype (Prefix (Expr)));
-                     Int_T   : constant Entity_Id := Base_Type (Target_Type);
-                     Last_I  : constant Uint :=
-                        Intval (High_Bound (Scalar_Range (Int_T)));
-                     Last_E  : Uint;
+                     Enum_T : constant Entity_Id :=
+                                Root_Type (Etype (Prefix (Expr)));
+                     Int_T  : constant Entity_Id := Base_Type (Target_Type);
+                     Last_I : constant Uint      :=
+                                Intval (High_Bound (Scalar_Range (Int_T)));
+                     Last_E : Uint;
 
                   begin
-                     --  Character types have no explicit literals, we use
+                     --  Character types have no explicit literals, so we use
                      --  the known number of characters in the type.
 
                      if Root_Type (Enum_T) = Standard_Character then
@@ -3422,7 +3422,8 @@ package body Checks is
                         Last_E := UI_From_Int (65535);
 
                      else
-                        Last_E := Enumeration_Pos
+                        Last_E :=
+                          Enumeration_Pos
                             (Entity (High_Bound (Scalar_Range (Enum_T))));
                      end if;
 
diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb
index 862e85b..eb73d03 100644
--- a/gcc/ada/contracts.adb
+++ b/gcc/ada/contracts.adb
@@ -53,11 +53,6 @@ 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;
@@ -68,6 +63,11 @@ package body Contracts is
    --  is reached. Freeze_Id is the entity of some related context which caused
    --  freezing up to node Freeze_Nod.
 
+   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 Expand_Subprogram_Contract (Body_Id : Entity_Id);
    --  Expand the contracts of a subprogram body and its correspoding spec (if
    --  any). This routine processes all [refined] pre- and postconditions as
@@ -1253,6 +1253,490 @@ package body Contracts is
       Restore_SPARK_Mode (Mode);
    end Analyze_Task_Contract;
 
+   -------------------------------------------------
+   -- Build_And_Analyze_Contract_Only_Subprograms --
+   -------------------------------------------------
+
+   procedure Build_And_Analyze_Contract_Only_Subprograms (L : List_Id) is
+      procedure Analyze_Contract_Only_Subprograms;
+      --  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 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);
+
+         Missing_Body_Name : constant Name_Id :=
+                               New_External_Name (Chars (E), "__missing_body");
+
+         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 Skip_Contract_Only_Subprogram (E : Entity_Id) return Boolean;
+         --  Return True for cases where the wrapper is not needed or we cannot
+         --  build it.
+
+         ------------------------------
+         -- Build_Missing_Body_Decls --
+         ------------------------------
+
+         function Build_Missing_Body_Decls return List_Id is
+            Spec : constant Node_Id := Declaration_Node (E);
+            Decl : Node_Id;
+            Prag : Node_Id;
+
+         begin
+            Decl :=
+              Make_Subprogram_Declaration (Loc, Copy_Subprogram_Spec (Spec));
+            Set_Chars (Defining_Entity (Decl), Missing_Body_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, Missing_Body_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
+            Parms := New_List;
+
+            --  Build parameter list that we need
+
+            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, Missing_Body_Name),
+                       Parameter_Associations => Parms));
+
+            else
+               return
+                 Make_Procedure_Call_Statement (Loc,
+                   Name                   =>
+                     Make_Identifier (Loc, Missing_Body_Name),
+                   Parameter_Associations => Parms);
+            end if;
+         end Build_Missing_Body_Subprogram_Call;
+
+         -----------------------------------
+         -- 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;
+
+            --  Start of processing for Depends_On_Enclosing_Private_Type
+
+            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 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 Convention (E) = Convention_Protected
+            then
+               return True;
+
+            --  We do not support building the contract-only subprogram 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.
+
+            elsif 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 it.
+
+         if Skip_Contract_Only_Subprogram (E) 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 :=
+                     New_External_Name (Chars (E), "__contract_only");
+            Id   : Entity_Id;
+            Bod  : Node_Id;
+
+         begin
+            Bod :=
+              Make_Subprogram_Body (Loc,
+                Specification              =>
+                  Copy_Subprogram_Spec (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;
+         New_Subp : Node_Id;
+         Result   : List_Id := No_List;
+         Subp_Id  : Entity_Id;
+
+      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_Protected_Definition,
+                             N_Task_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;
+   end Build_And_Analyze_Contract_Only_Subprograms;
+
    -----------------------------
    -- Create_Generic_Contract --
    -----------------------------
@@ -2679,565 +3163,4 @@ 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/scil_ll.adb b/gcc/ada/scil_ll.adb
index eed0d1a..bf9ded7 100644
--- a/gcc/ada/scil_ll.adb
+++ b/gcc/ada/scil_ll.adb
@@ -35,13 +35,6 @@ 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
@@ -108,27 +101,6 @@ package body SCIL_LL is
       end if;
    end Get_Contract_Only_Body;
 
-   ---------------------------------
-   -- Get_Contract_Only_Body_Name --
-   ---------------------------------
-
-   function Get_Contract_Only_Body_Name (E : Entity_Id) return Name_Id is
-   begin
-      return Name_Find (Get_Name_String (Chars (E)) &
-                          Contract_Only_Body_Suffix);
-   end Get_Contract_Only_Body_Name;
-
-   -----------------------------------------
-   -- Get_Contract_Only_Missing_Body_Name --
-   -----------------------------------------
-
-   function Get_Contract_Only_Missing_Body_Name (E : Entity_Id)
-      return Name_Id is
-   begin
-      return Name_Find (Get_Name_String (Chars (E)) &
-                          Contract_Only_Missing_Body_Suffix);
-   end Get_Contract_Only_Missing_Body_Name;
-
    -------------------
    -- Get_SCIL_Node --
    -------------------
diff --git a/gcc/ada/scil_ll.ads b/gcc/ada/scil_ll.ads
index bfac1a0..bebe0e7 100644
--- a/gcc/ada/scil_ll.ads
+++ b/gcc/ada/scil_ll.ads
@@ -32,17 +32,10 @@
 --  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