[Ada] Extra semantic rules for aspect Abstract_State and aspect Global

[Arnaud Charlet <charlet at adacore dot com>]

This patch implements the following formal verification rules:

A package_declaration of generic_package_declaration shall have a completion (a
body) if it contains a non-null Abstract_State aspect specification.

If a subprogram is nested within another and if the Global aspect specification
of the outer subprogram has an entity denoted by a global_item with a
mode_specification of Input, then a global_item of the Global aspect
specification of the inner subprogram shall not denote the same entity with a
mode_selector of In_Out or Out.

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

--  completion.ads

package Completion is
   package OK_1 with Abstract_State => null is
   end OK_1;

   package OK_2 with Abstract_State => State_OK_2 is
   end OK_2;

   package Error_1 with Abstract_State => State_Error_1 is
   end Error_1;

   generic
      type Formal_Typ is private;
   package OK_3 with Abstract_State => null is
   end OK_3;

   generic
      type Formal_Typ is private;
   package OK_4 with Abstract_State => State_OK_4 is
   end OK_4;

   generic
      type Formal_Typ is private;
   package Error_2 with Abstract_State => State_Error_2 is
   end Error_2;
end Completion;

--  completion.adb

package body Completion is
   package body OK_2 is end OK_2;
   package body OK_4 is end OK_4;
end Completion;

--  nesting.ads

package Nesting
   with Abstract_State => ((Input_State  with Volatile, Input),
                           (Output_State with Volatile, Output))
is
   Input_Var  : Integer;
   Mixed_Var  : Integer;
   Output_Var : Integer;
end Nesting;

--  nesting.adb

package body Nesting is
   procedure Outer
   with Global =>
          (Input  => (Input_State,  Input_Var),
           Output => (Output_State, Output_Var),
           In_Out =>  Mixed_Var);

   procedure Outer is
      procedure OK_1
      with Global => (Output => (Mixed_Var, Output_State, Output_Var));

      procedure OK_2
      with Global => (In_Out => Mixed_Var);

      procedure Error_1
      with Global => (Output => (Input_State, Input_Var));

      procedure Error_2
      with Global => (In_Out => (Input_State, Input_Var));

      procedure OK_1 is begin null; end OK_1;
      procedure OK_2 is begin null; end OK_2;
      procedure Error_1 is begin null; end Error_1;
      procedure Error_2 is begin null; end Error_2;
   begin
      null;
   end Outer;
end Nesting;

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

$ gcc -c -gnat12 -gnatd.V completion.adb
$ gcc -c -gnat12 -gnatd.V nesting.adb
completion.adb:1:14: missing body for "Error_1" declared at completion.ads:8
completion.adb:1:14: missing body for "Error_2" declared at completion.ads:23
nesting.adb:16:34: global item of mode In_Out or Output cannot reference
  Volatile Input state
nesting.adb:16:47: global item "Input_Var" cannot have mode In_Out or Output
nesting.adb:16:47: item already appears as input of subprogram "Outer"
nesting.adb:19:34: global item of mode In_Out or Output cannot reference
  Volatile Input state
nesting.adb:19:47: global item "Input_Var" cannot have mode In_Out or Output
nesting.adb:19:47: item already appears as input of subprogram "Outer"

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

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

	* einfo.adb (Set_Abstract_States): The attribute now applies
	to generic packages.
	* sem_ch4.adb (Referenced): Moved to sem_util.
	* sem_ch7.adb (Unit_Requires_Body): A [generic] package with
	a non-null abstract state needs a body.
	* sem_prag.adb (Analyze_Depends_In_Decl_Part): Update the calls
	to Collect_Subprogram_Inputs_Outputs.
	(Analyze_Global_Item): Verify the proper usage of an item with mode
	In_Out or Output relative to the enclosing context.
	(Analyze_Pragma): Abstract_State can now be applied to a generic
	package. Do not reset the Analyzed flag for pragmas Depends and Global
	as this is not needed.
	(Appears_In): Moved to library level.
	(Check_Mode_Restiction_In_Enclosing_Context): New routine.
	(Collect_Subprogram_Inputs_Outputs): Moved to library level. Add
	formal parameters Subp_Id, Subp_Inputs, Subp_Outputs and Global
	seen along with comments on usage.
	* sem_util.ads, sem_util.adb (Referenced): New routine.

Attachment: difs
Description: Text document