[Ada] Aspect Global

[Arnaud Charlet <charlet at adacore dot com>]

This patch provides the initial implementation of aspect Global. This construct
is intended for formal verification proofs.

The syntax of the aspect is as follows:

   global_specification ::= (moded_global_list {, moded_global_list})
                            | global_list
                            | null
   moded_global_list    ::= mode_selector => global_list
   global_list          ::= global_item
                            | (global_item {, global_item})
   mode_selector        ::= Input | Output | In_Out | Contract_In
   global_item          ::= name

The semantics of the aspect are as follows:

A global_item of a subprogram shall be a stand alone variable object [that is,
it is not part of a larger object] or it shall be a state abstraction. Each
mode_selector shall occur at most once in a single Global aspect. A function
subprogram may not have a mode_selector of Output or In_Out in its Global
aspect. Global_items in the same Global aspect shall denote distinct entities.  
A global item occurring in a Global aspect of a subprogram aspect specification
shall not have the same defining_identifier as a formal parameter of the
subprogram. A global item of mode in out or out shall not be a Volatile Input
state abstraction (see Abstract State Aspect). A global item of mode in or in
out shall not be a Volatile Output state abstraction.

This patch also corrects the timing of pragma Abstract_State analysis.

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

--  semantics.ads

package Semantics
   with Abstract_State =>
     ((Input_State  with Volatile, Input),
      (Output_State with Volatile, Output))
is
   type Composite is record
      Comp : Integer;
   end record;
   Var : Composite;

   type Composite_Array is array (1 .. 5) of Composite;
   Arr : Composite_Array;

   procedure Dummy_Proc;
   procedure OK_1
     with Global => (Var, Input_State);
   procedure Error_1
     with Global =>
       (Var.Comp,
        Arr (2),
        Dummy_Proc);
   procedure OK_2
     with Global =>
       (Input  => (Var, Input_State),
        Output => Arr);
   procedure Error_2
     with Global =>
       (Input       => Var,
        Contract_In => Input_State,
        Input       => Arr);
   function OK_3 return Boolean
     with Global =>
       (Input       => Var,
        Contract_In => Input_State);
   function Error_3 return Boolean
     with Global =>
       (In_Out => Arr,
        Output => Var);
   procedure Error_4
     with Global =>
       (Input  => Semantics.Var,
        Output => Var);
   function Error_5 (Formal : Boolean) return Boolean
     with Global => Formal;
   procedure Error_6
     with Global => (In_Out => Input_State);
   procedure Error_7
     with Global => (Output => Input_State);
   procedure Error_8
     with Global => (In_Out => Output_State);
   procedure Error_9
     with Global => (Input => Output_State);
   procedure Error_10
     with Global => Output_State;
   procedure OK_4
     with Global => null;
   procedure Error_11
     with Global => (null, Var);
   procedure Error_12
     with Global => (Var, null, Arr);
   procedure Error_13
     with Global => (Var, null);
end Semantics;

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

$ gcc -c -gnat12 -gnatd.V semantics.ads
semantics.ads:19:12: global item must denote variable or state
semantics.ads:20:09: global item must denote variable or state
semantics.ads:21:09: global item must denote variable or state
semantics.ads:30:09: duplicate global mode
semantics.ads:37:09: global mode "In_Out" not applicable to functions
semantics.ads:38:09: global mode "Output" not applicable to functions
semantics.ads:42:19: duplicate global item
semantics.ads:44:21: global item cannot reference formal parameter
semantics.ads:46:32: global item of mode In_Out or Output cannot reference Volatile Input state
semantics.ads:48:32: global item of mode In_Out or Output cannot reference Volatile Input state
semantics.ads:50:32: global item of mode In_Out or Input cannot reference Volatile Output state
semantics.ads:52:31: global item of mode In_Out or Input cannot reference Volatile Output state
semantics.ads:54:21: global item of mode In_Out or Input cannot reference Volatile Output state
semantics.ads:58:22: cannot mix null and non-null global items
semantics.ads:60:27: cannot mix null and non-null global items
semantics.ads:62:27: cannot mix null and non-null global items

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

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

	* aspects.adb, aspects.ads: Add Aspect_Global to all relevant tables.
	* par-prag.adb: Add pragma Global to the list of pragmas that
	do not need special processing by the parser.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Convert aspect
	Global into a pragma without any form of legality checks. The
	work is done by Analyze_Pragma. The aspect and pragma are both
	marked as needing delayed processing.  Insert the corresponding
	pragma of aspect Abstract_State in the visible declarations of the
	related package.
	(Check_Aspect_At_Freeze_Point): Aspect Global
	does not need processing even though it is marked as delayed.
	Alphabetize the list on aspect names.
	* sem_prag.adb: Add a value for pragma Global in table Sig_Flags.
	(Analyze_Pragma): Add ??? comment about the grammar of pragma
	Abstract_State.  Move the error location from the pragma to the
	state to improve the quality of error placement.  Add legality
	checks for pragma Global.
	* snames.ads-tmpl Add the following specially recognized names

Attachment: difs
Description: Text document