This patch ensures that contract of subprogram body stubs are analyzed in
timely fashion.

------------
-- Source --
------------

--  pack.ads

package Pack
  with SPARK_Mode,
       Abstract_State => State,
       Initializes    => (Var_1, State)
is
   Var_1 : Integer := 0;

   procedure Double
     with Global => (In_Out => (State, Var_1));

   procedure Error_1
     with Global => (In_Out => State);
end Pack;

--  pack-double.adb

separate (Pack)

procedure Double with SPARK_Mode is
begin
   Var_1 := Var_1 * 2;
end Double;

--  pack-double_a.adb

separate (Pack)

procedure Double_A with SPARK_Mode is
begin
   Var_2 := Var_2 * 2;
end Double_A;

--  pack-error_1.adb

separate (Pack)

procedure Error_1 with SPARK_Mode is
begin
   null;
end Error_1;

--  pack-error_2.adb

separate (Pack)

procedure Error_2 with SPARK_Mode is
begin
   null;
end Error_2;

--  pack.adb

package body Pack
  with SPARK_Mode,
       Refined_State => (State => Var_2)
is
   Var_2 : Integer := 0;

   procedure Double is separate
     with Refined_Global => (In_Out => (Var_1, Var_2));

   procedure Double_A is separate
     with Global => (In_Out => Var_2);

   procedure Error_1 is separate
     with Refined_Global => (In_Out => Junk_1);

   procedure Error_2 is separate
     with Global => (In_Out => Junk_2);
end Pack;

----------------------------
-- Compilation and output --
----------------------------

$ gcc -c pack.adb
pack.adb:14:40: "Junk_1" is undefined
pack.adb:17:32: "Junk_2" is undefined

Tested on x86_64-pc-linux-gnu, committed on trunk

2014-06-11  Hristian Kirtchev  <kirtc...@adacore.com>

        * sem_ch3.adb Add with and use clause for Sem_Ch10.
        (Analyze_Declarations): Code reformatting. Analyze the contract
        of a subprogram body stub at the end of the declarative region.
        * sem_ch6.adb (Analyze_Subprogram_Body_Contract): Spec_Id is
        now a variable. Do not process the body if its contract is not
        available. Account for subprogram body stubs when extracting
        the corresponding spec.
        * sem_ch6.ads (Analyze_Subprogram_Contract): Update the comment
        on usage.
        * sem_ch10.ads, sem_ch10.adb (Analyze_Subprogram_Body_Stub_Contract):
        New routine.
        * sem_prag.adb (Analyze_Depends_In_Decl_Part):
        Account for subprogram body stubs when extracting the
        corresponding spec.
        (Analyze_Global_In_Decl_List):
        Account for subprogram body stubs when extracting the
        corresponding spec.
        (Analyze_Refined_Depends_In_Decl_Part):
        Use Find_Related_Subprogram_Or_Body to retrieve the declaration
        of the related body. Spec_Is now a variable. Account for
        subprogram body stubs when extracting the corresponding spec.
        (Analyze_Refined_Global_In_Decl_Part): Use
        Find_Related_Subprogram_Or_Body to retrieve the declaration
        of the related body. Spec_Is now a variable. Account for
        subprogram body stubs when extracting the corresponding spec.
        (Collect_Subprogram_Inputs_Output): Account for subprogram body
        stubs when extracting the corresponding spec.

Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb (revision 211448)
+++ sem_ch3.adb (working copy)
@@ -57,6 +57,7 @@
 with Sem_Ch6;  use Sem_Ch6;
 with Sem_Ch7;  use Sem_Ch7;
 with Sem_Ch8;  use Sem_Ch8;
+with Sem_Ch10; use Sem_Ch10;
 with Sem_Ch13; use Sem_Ch13;
 with Sem_Dim;  use Sem_Dim;
 with Sem_Disp; use Sem_Disp;
@@ -2371,13 +2372,16 @@
          if Nkind (Decl) = N_Object_Declaration then
             Analyze_Object_Contract (Defining_Entity (Decl));
 
+         elsif Nkind_In (Decl, N_Abstract_Subprogram_Declaration,
+                               N_Subprogram_Declaration)
+         then
+            Analyze_Subprogram_Contract (Defining_Entity (Decl));
+
          elsif Nkind (Decl) = N_Subprogram_Body then
             Analyze_Subprogram_Body_Contract (Defining_Entity (Decl));
 
-         elsif Nkind_In (Decl, N_Subprogram_Declaration,
-                               N_Abstract_Subprogram_Declaration)
-         then
-            Analyze_Subprogram_Contract (Defining_Entity (Decl));
+         elsif Nkind (Decl) = N_Subprogram_Body_Stub then
+            Analyze_Subprogram_Body_Stub_Contract (Defining_Entity (Decl));
          end if;
 
          Next (Decl);
Index: sem_ch10.adb
===================================================================
--- sem_ch10.adb        (revision 211445)
+++ sem_ch10.adb        (working copy)
@@ -1879,6 +1879,39 @@
       end if;
    end Analyze_Protected_Body_Stub;
 
+   -------------------------------------------
+   -- Analyze_Subprogram_Body_Stub_Contract --
+   -------------------------------------------
+
+   procedure Analyze_Subprogram_Body_Stub_Contract (Stub_Id : Entity_Id) is
+      Stub_Decl : constant Node_Id   := Parent (Parent (Stub_Id));
+      Spec_Id   : constant Entity_Id := Corresponding_Spec_Of_Stub (Stub_Decl);
+
+   begin
+      --  A subprogram body stub may act as its own spec or as the completion
+      --  of a previous declaration. Depending on the context, the contract of
+      --  the stub may contain two sets of pragmas.
+
+      --  The stub is a completion, the applicable pragmas are:
+      --    Contract_Cases
+      --    Depends
+      --    Global
+      --    Postcondition
+      --    Precondition
+      --    Test_Case
+
+      if Present (Spec_Id) then
+         Analyze_Subprogram_Body_Contract (Stub_Id);
+
+      --  The stub acts as its own spec, the applicable pragmas are:
+      --    Refined_Depends
+      --    Refined_Global
+
+      else
+         Analyze_Subprogram_Contract (Stub_Id);
+      end if;
+   end Analyze_Subprogram_Body_Stub_Contract;
+
    ----------------------------------
    -- Analyze_Subprogram_Body_Stub --
    ----------------------------------
Index: sem_ch10.ads
===================================================================
--- sem_ch10.ads        (revision 211445)
+++ sem_ch10.ads        (working copy)
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1992-2010, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2014, 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- --
@@ -33,6 +33,19 @@
    procedure Analyze_Protected_Body_Stub                (N : Node_Id);
    procedure Analyze_Subunit                            (N : Node_Id);
 
+   procedure Analyze_Subprogram_Body_Stub_Contract (Stub_Id : Entity_Id);
+   --  Analyze all delayed aspects chained on the contract of a subprogram body
+   --  stub Stub_Id as if they appeared at the end of a declarative region. The
+   --  aspects in question are:
+   --    Contract_Cases
+   --    Depends
+   --    Global
+   --    Postcondition
+   --    Precondition
+   --    Refined_Depends
+   --    Refined_Global
+   --    Test_Case
+
    procedure Install_Context (N : Node_Id);
    --  Installs the entities from the context clause of the given compilation
    --  unit into the visibility chains. This is done before analyzing a unit.
Index: sem_prag.adb
===================================================================
--- sem_prag.adb        (revision 211448)
+++ sem_prag.adb        (working copy)
@@ -1700,11 +1700,13 @@
       --  Refined_Depends.
 
       if Nkind (Subp_Decl) = N_Subprogram_Body
-        and then not Acts_As_Spec (Subp_Decl)
+        and then Present (Corresponding_Spec (Subp_Decl))
       then
          Spec_Id := Corresponding_Spec (Subp_Decl);
 
-      elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub then
+      elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub
+        and then Present (Corresponding_Spec_Of_Stub (Subp_Decl))
+      then
          Spec_Id := Corresponding_Spec_Of_Stub (Subp_Decl);
 
       else
@@ -2327,11 +2329,13 @@
       --  Refined_Global.
 
       if Nkind (Subp_Decl) = N_Subprogram_Body
-        and then not Acts_As_Spec (Subp_Decl)
+        and then Present (Corresponding_Spec (Subp_Decl))
       then
          Spec_Id := Corresponding_Spec (Subp_Decl);
 
-      elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub then
+      elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub
+        and then Present (Corresponding_Spec_Of_Stub (Subp_Decl))
+      then
          Spec_Id := Corresponding_Spec_Of_Stub (Subp_Decl);
 
       else
@@ -22623,7 +22627,7 @@
 
       --  Local variables
 
-      Body_Decl : constant Node_Id := Parent (N);
+      Body_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N);
       Errors    : constant Nat     := Serious_Errors_Detected;
       Refs      : constant Node_Id :=
                     Get_Pragma_Arg (First (Pragma_Argument_Associations (N)));
@@ -22641,7 +22645,12 @@
          return;
       end if;
 
-      Spec_Id := Corresponding_Spec (Body_Decl);
+      if Nkind (Body_Decl) = N_Subprogram_Body_Stub then
+         Spec_Id := Corresponding_Spec_Of_Stub (Body_Decl);
+      else
+         Spec_Id := Corresponding_Spec (Body_Decl);
+      end if;
+
       Depends := Get_Pragma (Spec_Id, Pragma_Depends);
 
       --  Subprogram declarations lacks pragma Depends. Refined_Depends is
@@ -23390,11 +23399,11 @@
 
       --  Local variables
 
-      Body_Decl : constant Node_Id := Parent (N);
+      Body_Decl : constant Node_Id := Find_Related_Subprogram_Or_Body (N);
       Errors    : constant Nat     := Serious_Errors_Detected;
       Items     : constant Node_Id :=
                     Get_Pragma_Arg (First (Pragma_Argument_Associations (N)));
-      Spec_Id   : constant Entity_Id := Corresponding_Spec (Body_Decl);
+      Spec_Id   : Entity_Id;
 
    --  Start of processing for Analyze_Refined_Global_In_Decl_Part
 
@@ -23407,6 +23416,12 @@
          return;
       end if;
 
+      if Nkind (Body_Decl) = N_Subprogram_Body_Stub then
+         Spec_Id := Corresponding_Spec_Of_Stub (Body_Decl);
+      else
+         Spec_Id := Corresponding_Spec (Body_Decl);
+      end if;
+
       Global := Get_Pragma (Spec_Id, Pragma_Global);
 
       --  The subprogram declaration lacks pragma Global. This renders
@@ -25323,10 +25338,11 @@
 
       --  Local variables
 
-      Formal  : Entity_Id;
-      Global  : Node_Id;
-      List    : Node_Id;
-      Spec_Id : Entity_Id;
+      Subp_Decl : constant Node_Id := Parent (Parent (Subp_Id));
+      Formal    : Entity_Id;
+      Global    : Node_Id;
+      List      : Node_Id;
+      Spec_Id   : Entity_Id;
 
    --  Start of processing for Collect_Subprogram_Inputs_Outputs
 
@@ -25335,8 +25351,16 @@
 
       --  Find the entity of the corresponding spec when processing a body
 
-      if Ekind (Subp_Id) = E_Subprogram_Body then
-         Spec_Id := Corresponding_Spec (Parent (Parent (Subp_Id)));
+      if Nkind (Subp_Decl) = N_Subprogram_Body
+        and then Present (Corresponding_Spec (Subp_Decl))
+      then
+         Spec_Id := Corresponding_Spec (Subp_Decl);
+
+      elsif Nkind (Subp_Decl) = N_Subprogram_Body_Stub
+        and then Present (Corresponding_Spec_Of_Stub (Subp_Decl))
+      then
+         Spec_Id := Corresponding_Spec_Of_Stub (Subp_Decl);
+
       else
          Spec_Id := Subp_Id;
       end if;
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb (revision 211448)
+++ sem_ch6.adb (working copy)
@@ -2031,21 +2031,27 @@
    --------------------------------------
 
    procedure Analyze_Subprogram_Body_Contract (Body_Id : Entity_Id) is
-      Body_Decl   : constant Node_Id   := Parent (Parent (Body_Id));
-      Spec_Id     : constant Entity_Id := Corresponding_Spec (Body_Decl);
+      Body_Decl   : constant Node_Id := Parent (Parent (Body_Id));
       Prag        : Node_Id;
       Ref_Depends : Node_Id := Empty;
       Ref_Global  : Node_Id := Empty;
+      Spec_Id     : Entity_Id;
 
    begin
       --  When a subprogram body declaration is illegal, its defining entity is
       --  left unanalyzed. There is nothing left to do in this case because the
       --  body lacks a contract.
 
-      if not Analyzed (Body_Id) then
+      if No (Contract (Body_Id)) then
          return;
       end if;
 
+      if Nkind (Body_Decl) = N_Subprogram_Body_Stub then
+         Spec_Id := Corresponding_Spec_Of_Stub (Body_Decl);
+      else
+         Spec_Id := Corresponding_Spec (Body_Decl);
+      end if;
+
       --  Locate and store pragmas Refined_Depends and Refined_Global since
       --  their order of analysis matters.
 
Index: sem_ch6.ads
===================================================================
--- sem_ch6.ads (revision 211445)
+++ sem_ch6.ads (working copy)
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1992-2013, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2014, 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- --
@@ -57,6 +57,8 @@
    --  as if they appeared at the end of a declarative region. The aspects in
    --  question are:
    --    Contract_Cases
+   --    Depends
+   --    Global
    --    Postcondition
    --    Precondition
    --    Test_Case

Reply via email to