[Ada] Proper placement and analysis of aspects/pragmas Depends and Global

[Arnaud Charlet <charlet at adacore dot com>]

This patch reimplements the analysis and expansion of aspects/pragmas Depends
and Global to mimic the mechanism for Postconditions. The two constructs now
appear on a special list which is part of a subprogram's contract. The items
are analyzed at the end of a declarative part.

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

--  small.ads

package Small is
   pragma Elaborate_Body (Small);
end Small;

--  small.adb

package body Small is
   procedure Ineffective_Statements (Export : out Integer) is
      Temp : Integer;

      procedure Initialize_Temp
        with Global  => (Output => Temp),
             Depends => (Temp => null)
      is
      begin
         Temp := 0;
      end Initialize_Temp;

      procedure Edit_Temp
        with Global  => (Output => Temp),
             Depends => (Temp => null)
      is
      begin
         Temp := 1;
      end Edit_Temp;

   begin
      Initialize_Temp;
      Edit_Temp;
      Export := Temp;
   end Ineffective_Statements;
end Small;

-----------------
-- Compilation --
-----------------

$ gcc -c -gnat12 -gnatd.V -gnatdg small.adb
Source recreated from tree for Small (body)
-------------------------------------------


package body small is

   procedure small__ineffective_statements (export : out integer) is
      temp : integer;

      procedure small__ineffective_statements__initialize_temp is
         pragma global ((
            output => temp));
         pragma depends ((
            temp => null));
      begin
         temp := 0;
         return;
      end small__ineffective_statements__initialize_temp
        with global => (
                output => temp),
             depends => (
                temp => null);

      procedure small__ineffective_statements__edit_temp is
         pragma global ((
            output => temp));
         pragma depends ((
            temp => null));
      begin
         temp := 1;
         return;
      end small__ineffective_statements__edit_temp
        with global => (
                output => temp),
             depends => (
                temp => null);
   begin
      small__ineffective_statements__initialize_temp;
      small__ineffective_statements__edit_temp;
      export := temp;
      return;
   end small__ineffective_statements;
begin
   null;
end small;

Source recreated from tree for Small (spec)
-------------------------------------------

small_E : short_integer := 0;

package small is
   pragma elaborate_body (small);
end small;

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

2013-04-23  Hristian Kirtchev  <kirtchev@adacore.com>

	* exp_ch9.adb (Build_PPC_Wrapper): Correct the traversal of
	pre- and post-conditions.
	(Expand_N_Task_Type_Declaration):
	Use the correct attribute to check for pre- and post-conditions.
	* exp_ch13.adb (Expand_N_Freeze_Entity): Correct the traversal of
	pre- and post-conditions.  Analyze delayed classification items.
	* freeze.adb (Freeze_Entity): Use the correct attribute to
	check for pre- and post- conditions.
	* sem_ch3.adb (Analyze_Declarations): Correct the traversal
	of pre- and post-conditions as well as contract- and
	test-cases. Analyze delayed pragmas Depends and Global.
	* sem_ch6.adb (Check_Subprogram_Contract): Use the correct
	attribute to check for pre- and post-conditions, as well as
	contract-cases and test-cases.	(List_Inherited_Pre_Post_Aspects):
	Correct the traversal of pre- and post- conditions.
	(Process_Contract_Cases): Update the comment on usage. Correct
	the traversal of contract-cases.
	(Process_Post_Conditions): Update the comment on usage. Correct the
	traversal of pre- and post-conditions.
	(Process_PPCs): Correct the traversal of pre- and post-conditions.
	(Spec_Postconditions): Use the correct
	attribute to check for pre- and post- conditions, as well as
	contract-cases and test-cases.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Reimplement the
	actions related to aspects Depends and Global. Code refactoring
	for pre- and post-conditions.
	(Insert_Delayed_Pragma): New routine.
	* sem_prag.adb (Add_Item): New routine.
	(Analyze_Depends_In_Decl_Part): New routine.
	(Analyze_Global_In_Decl_Part): New routine.
	(Analyze_Pragma): Reimplement the actions related to aspects Depends and
	Global. Verify that a body acts as a spec for pragma Contract_Cases.
	(Chain_PPC): Use Add_Contract_Item to chain a pragma.
	(Chain_CTC): Correct the traversal of contract-
	and test-cases. Use Add_Contract_Item to chain a pragma.
	(Chain_Contract_Cases): Correct the traversal of contract-
	and test-cases. Use Add_Contract_Item to chain a pragma.
	(Check_Precondition_Postcondition): Update the comment on usage.
	(Check_Test_Case): Update the comment on usage.
	* sem_prag.ads (Analyze_Depends_In_Decl_Part): New routine.
	(Analyze_Global_In_Decl_Part): New routine.
	* sem_util.ads, sem_util.adb (Add_Contract_Item): New routine.
	* sinfo.adb (Classifications): New routine.
	(Contract_Test_Cases): New routine.
	(Pre_Post_Conditions): New routine.
	(Set_Classifications): New routine.
	(Set_Contract_Test_Cases): New routine.
	(Set_Pre_Post_Conditions): New routine.
	(Set_Spec_CTC_List): Removed.
	(Set_Spec_PPC_List): Removed.
	(Spec_CTC_List): Removed.
	(Spec_PPC_List): Removed.
	* sinfo.ads: Update the structure of N_Contruct along with all
	related comments.
	(Classifications): New routine and pragma Inline.
	(Contract_Test_Cases): New routine and pragma Inline.
	(Pre_Post_Conditions): New routine and pragma Inline.
	(Set_Classifications): New routine and pragma Inline.
	(Set_Contract_Test_Cases): New routine and pragma Inline.
	(Set_Pre_Post_Conditions): New routine and pragma Inline.
	(Set_Spec_CTC_List): Removed.
	(Set_Spec_PPC_List): Removed.
	(Spec_CTC_List): Removed.
	(Spec_PPC_List): Removed.

Attachment: difs
Description: Text document