contracts.adb (Build_Postconditions_Procedure): Code cleanup.

2016-04-20  Javier Miranda  <miranda@adacore.com>

	* contracts.adb (Build_Postconditions_Procedure): Code cleanup.
	* ghost.adb (Os_OK_Ghost_Context.Is_OK_Declaration): Handle the
	declaration of the internally built _postcondition procedure.

From-SVN: r235245

3 files changed, 57 insertions, 45 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index fe429f1..db327f3 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,9 @@
+2016-04-20  Javier Miranda  <miranda@adacore.com>
+
+	* contracts.adb (Build_Postconditions_Procedure): Code cleanup.
+	* ghost.adb (Os_OK_Ghost_Context.Is_OK_Declaration): Handle the
+	declaration of the internally built _postcondition procedure.
+
 2016-04-20  Arnaud Charlet  <charlet@adacore.com>
 
 	* snames.ads-tmpl (Internal_Attribute_Id, Attribute_Class_Array): Fix
diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb
index a5f8bc3..af6264c 100644
--- a/gcc/ada/contracts.adb
+++ b/gcc/ada/contracts.adb
@@ -1749,8 +1749,7 @@ package body Contracts is
          end if;
 
          Proc_Id := Make_Defining_Identifier (Loc, Name_uPostconditions);
-         Set_Debug_Info_Needed   (Proc_Id);
-         Set_Postconditions_Proc (Subp_Id, Proc_Id);
+         Set_Debug_Info_Needed (Proc_Id);
 
          --  The related subprogram is a function: create the specification of
          --  parameter _Result.
@@ -1786,51 +1785,47 @@ package body Contracts is
          --  the postconditions: this would cause confusing debug info to be
          --  produced, interfering with coverage-analysis tools.
 
-         Proc_Bod :=
-           Make_Subprogram_Body (Loc,
-             Specification              =>
+         declare
+            Proc_Decl    : Node_Id;
+            Proc_Decl_Id : Entity_Id;
+            Proc_Spec    : Node_Id;
+         begin
+            Proc_Spec :=
                Make_Procedure_Specification (Loc,
                  Defining_Unit_Name       => Proc_Id,
-                 Parameter_Specifications => Params),
-
-             Declarations               => Empty_List,
-             Handled_Statement_Sequence =>
-               Make_Handled_Sequence_Of_Statements (Loc,
-                 Statements => Stmts,
-                 End_Label  => Make_Identifier (Loc, Chars (Proc_Id))));
-
-         Insert_Before_First_Source_Declaration (Proc_Bod);
+                 Parameter_Specifications => Params);
 
-         --  Force the front-end inlining of _PostConditions when generating
-         --  C code, since its body may have references to itypes defined in
-         --  the enclosing subprogram, thus causing problems for the unnested
-         --  routines. For this purpose its declaration with proper decoration
-         --  for inlining is needed.
+            Proc_Decl := Make_Subprogram_Declaration (Loc, Proc_Spec);
+            Proc_Decl_Id := Defining_Entity (Specification (Proc_Decl));
+            Set_Postconditions_Proc (Subp_Id, Proc_Decl_Id);
 
-         if Generate_C_Code then
-            declare
-               Proc_Decl    : Node_Id;
-               Proc_Decl_Id : Entity_Id;
-
-            begin
-               Proc_Decl :=
-                 Make_Subprogram_Declaration (Loc,
-                   Specification =>
-                     Copy_Subprogram_Spec (Specification (Proc_Bod)));
-               Insert_Before (Proc_Bod, Proc_Decl);
+            --  Force the front end inlining of _PostConditions when generating
+            --  C code since its body may have references to itypes defined in
+            --  the enclosing subprogram, thus causing problems to unnesting
+            --  routines.
 
-               Proc_Decl_Id := Defining_Entity (Specification (Proc_Decl));
+            if Generate_C_Code then
                Set_Has_Pragma_Inline (Proc_Decl_Id);
                Set_Has_Pragma_Inline_Always (Proc_Decl_Id);
                Set_Is_Inlined (Proc_Decl_Id);
+            end if;
 
-               Set_Postconditions_Proc (Subp_Id, Proc_Decl_Id);
-
-               Analyze (Proc_Decl);
-            end;
-         end if;
-
-         Analyze (Proc_Bod);
+            Insert_Before_First_Source_Declaration (Proc_Decl);
+            Analyze (Proc_Decl);
+
+            Proc_Bod :=
+              Make_Subprogram_Body (Loc,
+                Specification              =>
+                  Copy_Subprogram_Spec (Proc_Spec),
+                Declarations               => Empty_List,
+                Handled_Statement_Sequence =>
+                  Make_Handled_Sequence_Of_Statements (Loc,
+                    Statements => Stmts,
+                    End_Label  => Make_Identifier (Loc, Chars (Proc_Id))));
+
+            Insert_Before_First_Source_Declaration (Proc_Bod);
+            Analyze (Proc_Bod);
+         end;
       end Build_Postconditions_Procedure;
 
       ----------------------------
diff --git a/gcc/ada/ghost.adb b/gcc/ada/ghost.adb
index 9d01b6d..69865b5 100644
--- a/gcc/ada/ghost.adb
+++ b/gcc/ada/ghost.adb
@@ -254,15 +254,26 @@ package body Ghost is
             then
                Subp_Id := Corresponding_Spec (Decl);
 
-               --  The original context is an expression function that has
-               --  been split into a spec and a body. The context is OK as
-               --  long as the initial declaration is Ghost.
-
                if Present (Subp_Id) then
-                  Subp_Decl := Original_Node (Unit_Declaration_Node (Subp_Id));
 
-                  if Nkind (Subp_Decl) = N_Expression_Function then
-                     return Is_Subject_To_Ghost (Subp_Decl);
+                  --  The context is the internally built _postconditions
+                  --  subprogram, which it is OK because the real check was
+                  --  done before expansion activities.
+
+                  if Chars (Subp_Id) = Name_uPostconditions then
+                     return True;
+
+                  else
+                     Subp_Decl :=
+                       Original_Node (Unit_Declaration_Node (Subp_Id));
+
+                     --  The original context is an expression function that
+                     --  has been split into a spec and a body. The context is
+                     --  OK as long as the initial declaration is Ghost.
+
+                     if Nkind (Subp_Decl) = N_Expression_Function then
+                        return Is_Subject_To_Ghost (Subp_Decl);
+                     end if;
                   end if;
 
                --  Otherwise this is either an internal body or an internal