Patchwork [Ada] Aspect Abstract_State

login
register
mail settings
Submitter Arnaud Charlet
Date Jan. 3, 2013, 1:07 p.m.
Message ID <20130103130712.GA32317@adacore.com>
Download mbox | patch
Permalink /patch/209247/
State New
Headers show

Comments

Arnaud Charlet - Jan. 3, 2013, 1:07 p.m.
This patch provides the initial implementation of aspect Abstract_State. This
construct is intended for formal verification proofs.

The syntax of the aspect is as follows:

   abstract_state_list        ::=
      null
      | state_name_with_properties
      | (state_name_with_properties { , state_name_with_properties } )

   state_name_with_properties ::=
      state_name
      | ( state_name with property_list )

   property_list              ::= property { , property }
   property                   ::= simple_property
                                  | name_value_property
   simple_property            ::= identifier
   name_value_property        ::= identifier => expression
   state_name                 ::= defining_identifier

The semantics of the aspect are as follows:

The identifier of a simple_property shall be Volatile, Input, or Output. There
shall be at most one occurrence of the identifiers Volatile, Input and Output
in a single property_list. If a property_list includes Volatile, then it shall
also include exactly one of Input or Output. If a property_list includes either
Input or Output, then it shall also include Volatile. The identifier of a
name_value_property shall be Integrity. If a property_list includes Integrity
then it shall be the final property in the list.

Each state_name occurring in an Abstract_State aspect specification for a given
package P introduces an implicit declaration of a state abstraction entity.
This implicit declaration occurs at the beginning of the visible part of P.
This implicit declaration requires completion.

A state abstraction shall only be named in contexts where this is explicitly
permitted (e.g., as part of a Globals aspect specification), but this is not a
name resolution rule. Thus, the declaration of a state abstraction has the same
visibility as any other declaration. A state abstraction is not an object; it
does not have a type. The completion of a state abstraction declared in a
package aspect_specification can only be provided as part of a Refined_State
aspect specification within the body of the package.

A null abstract_state_list specifies that a package contains no hidden state or
variables declared in its visible_part.

A variable declared in the visible_part of a package implicitly declares a
state abstraction entity with the same identifier as the defining_identifier of
the variable. The variable declaration acts as the completion of the state
abstraction. The implicitly declared state abstraction is only visible in a
limited view of the package.

A volatile state abstraction is one declared with a property list which
includes the Volatile property, and either Input or Output. A Volatile Input or
Output state abstraction represents a sequence of state changes brought about
by reading or writing successive values to or from a volatile variable.

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

--  semantics.ads

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

   package OK_2
     with Abstract_State =>
       (S_1,
       (S_2 with Volatile, Input, Integrity => 1),
       (S_3 with Output, Volatile, Integrity => 2))
   is end OK_2;

   package Error_1
     with Abstract_State =>
       (S_1,
        S_1,                        --  duplicate state name
        123,                        --  junk state name
       (123 with Input, Volatile),  --  junk state name
       (S_2 with Junk_Name),        --  junk property
       (S_3 with Input, Input),     --  duplicate property
       (S_4 with Input),            --  no Volatile
       (S_5 with Output),           --  no Volatile
       (S_6 with Volatile),         --  neither Input nor Output
       (S_7 with Volatile, Input, Output),  --  can't have Input and Output
       (S_8 with Integrity => Junk_Value),  --  has to be integer literal
       null)                        --  can't have null or any of the above
   is end Error_1;
end Semantics;

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

$ gcc -c -gnatc -gnat12 -gnatd.V semantics.ads
semantics.ads:14:11: malformed abstract state declaration
semantics.ads:16:09: "S_1" conflicts with declaration at line 15
semantics.ads:18:09: state name must be an identifier
semantics.ads:19:18: invalid state property
semantics.ads:20:25: duplicate state property
semantics.ads:21:08: properties Input and Output require Volatile
semantics.ads:22:08: properties Input and Output require Volatile
semantics.ads:23:08: property Volatile requires exactly one Input or Output
semantics.ads:24:08: property Volatile requires exactly one Input or Output
semantics.ads:25:31: integrity level must be an integer literal
semantics.ads:26:08: package "Error_1" has non-null abstract state

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

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

	* aspects.adb, aspects.ads: Add Aspect_Abstract_State to all the
	relevant tables.
	* einfo.ads, einfo.adb: Add Integrity_Level and Refined_State to
	the description of fields (Abstract_States): New routine.
	(Integrity_Level): New routine.
	(Has_Property): New routine.
	(Is_Input_State): New routine.
	(Is_Null_State): New routine.
	(Is_Output_State): New routine.
	(Is_Volatile_State): New routine.
	(Refined_State): New routine.
	(Set_Abstract_States): New routine.
	(Set_Integrity_Level): New routine.
	(Set_Refined_State): New routine.
	(Write_Field8_Name): Add proper output for E_Abstract_State.
	(Write_Field9_Name): Add proper output for E_Abstract_State.
	(Write_Field25_Name): Add proper output for E_Package.
	* lib-xref.ads: Add new letter for an abstract state.
	* par-prag.adb: Add pragma Abstract_State to the list of pragma
	that do not need special processing by the parser.
	* sem_ch13.adb (Analyze_Aspect_Specifications): Convert
	aspect Abstract_State into a pragma without any form
	of legality checks. The work is done by Analyze_Pragma.
	(Check_Aspect_At_Freeze_Point): Aspect Abstract_State does not
	require delayed analysis.
	* sem_prag.adb: Add a value for pragma Abstract_State in table
	Sig_Flags.
	(Analyze_Pragma): Add legality checks for pragma
	Abstract_State. Analysis of individual states introduces a state
	abstraction entity into the visibility chain.
	* snames.ads-tmpl: Add new names for abstract state and
	integrity. Add new pragma id for abstract state.

Patch

Index: einfo.adb
===================================================================
--- einfo.adb	(revision 194847)
+++ einfo.adb	(working copy)
@@ -76,6 +76,7 @@ 
    --    Associated_Node_For_Itype       Node8
    --    Dependent_Instances             Elist8
    --    Hiding_Loop_Variable            Node8
+   --    Integrity_Level                 Uint8
    --    Mechanism                       Uint8 (but returns Mechanism_Type)
    --    Normalized_First_Bit            Uint8
    --    Postcondition_Proc              Node8
@@ -84,6 +85,7 @@ 
 
    --    Class_Wide_Type                 Node9
    --    Current_Value                   Node9
+   --    Refined_State                   Node9
    --    Renaming_Map                    Uint9
 
    --    Direct_Primitive_Operations     Elist10
@@ -535,6 +537,12 @@ 
    -- Local subprograms --
    -----------------------
 
+   function Has_Property
+     (State    : Entity_Id;
+      Prop_Nam : Name_Id) return Boolean;
+   --  Determine whether abstract state State has a particular property denoted
+   --  by the name Prop_Nam.
+
    function Rep_Clause (Id : E; Rep_Name : Name_Id) return N;
    --  Returns the attribute definition clause for Id whose name is Rep_Name.
    --  Returns Empty if no matching attribute definition clause found for Id.
@@ -549,6 +557,41 @@ 
       return F'Val (UI_To_Int (Uint10 (Base_Type (Id))));
    end Float_Rep;
 
+   ------------------
+   -- Has_Property --
+   ------------------
+
+   function Has_Property
+     (State    : Entity_Id;
+      Prop_Nam : Name_Id) return Boolean
+   is
+      Par  : constant Node_Id := Parent (State);
+      Prop : Node_Id;
+
+   begin
+      pragma Assert (Ekind (State) = E_Abstract_State);
+
+      --  States with properties appear as extension aggregates in the tree
+
+      if Nkind (Par) = N_Extension_Aggregate then
+         if Prop_Nam = Name_Integrity then
+            return Present (Component_Associations (Par));
+
+         else
+            Prop := First (Expressions (Par));
+            while Present (Prop) loop
+               if Chars (Prop) = Prop_Nam then
+                  return True;
+               end if;
+
+               Next (Prop);
+            end loop;
+         end if;
+      end if;
+
+      return False;
+   end Has_Property;
+
    ----------------
    -- Rep_Clause --
    ----------------
@@ -575,6 +618,12 @@ 
    -- Attribute Access Functions --
    --------------------------------
 
+   function Abstract_States (Id : E) return L is
+   begin
+      pragma Assert (Ekind (Id) = E_Package);
+      return Elist25 (Id);
+   end Abstract_States;
+
    function Accept_Address (Id : E) return L is
    begin
       return Elist21 (Id);
@@ -1662,6 +1711,12 @@ 
       return Node28 (Id);
    end Initialization_Statements;
 
+   function Integrity_Level (Id : E) return U is
+   begin
+      pragma Assert (Ekind (Id) = E_Abstract_State);
+      return Uint8 (Id);
+   end Integrity_Level;
+
    function Inner_Instances (Id : E) return L is
    begin
       return Elist23 (Id);
@@ -2534,6 +2589,12 @@ 
       return Flag227 (Id);
    end Referenced_As_Out_Parameter;
 
+   function Refined_State (Id : E) return E is
+   begin
+      pragma Assert (Ekind (Id) = E_Abstract_State);
+      return Node9 (Id);
+   end Refined_State;
+
    function Register_Exception_Call (Id : E) return N is
    begin
       pragma Assert (Ekind (Id) = E_Exception);
@@ -3084,6 +3145,12 @@ 
    --  it is possible to add assertions that specifically include the E_Void
    --  possibility, but in some cases, we just omit the assertions.
 
+   procedure Set_Abstract_States (Id : E; V : L) is
+   begin
+      pragma Assert (Ekind (Id) = E_Package);
+      Set_Elist25 (Id, V);
+   end Set_Abstract_States;
+
    procedure Set_Accept_Address (Id : E; V : L) is
    begin
       Set_Elist21 (Id, V);
@@ -4200,6 +4267,12 @@ 
       Set_Node28 (Id, V);
    end Set_Initialization_Statements;
 
+   procedure Set_Integrity_Level (Id : E; V : Uint) is
+   begin
+      pragma Assert (Ekind (Id) = E_Abstract_State);
+      Set_Uint8 (Id, V);
+   end Set_Integrity_Level;
+
    procedure Set_Inner_Instances (Id : E; V : L) is
    begin
       Set_Elist23 (Id, V);
@@ -5110,6 +5183,12 @@ 
       Set_Flag227 (Id, V);
    end Set_Referenced_As_Out_Parameter;
 
+   procedure Set_Refined_State (Id : E; V : E) is
+   begin
+      pragma Assert (Ekind (Id) = E_Abstract_State);
+      Set_Node9 (Id, V);
+   end Set_Refined_State;
+
    procedure Set_Register_Exception_Call (Id : E; V : N) is
    begin
       pragma Assert (Ekind (Id) = E_Exception);
@@ -6364,6 +6443,37 @@ 
         and then Chars (Id) = Name_uFinalizer;
    end Is_Finalizer;
 
+   --------------------
+   -- Is_Input_State --
+   --------------------
+
+   function Is_Input_State (Id : E) return B is
+   begin
+      return
+        Ekind (Id) = E_Abstract_State and then Has_Property (Id, Name_Input);
+   end Is_Input_State;
+
+   -------------------
+   -- Is_Null_State --
+   -------------------
+
+   function Is_Null_State (Id : E) return B is
+   begin
+      return
+        Ekind (Id) = E_Abstract_State
+          and then Nkind (Parent (Id)) = N_Null;
+   end Is_Null_State;
+
+   ---------------------
+   -- Is_Output_State --
+   ---------------------
+
+   function Is_Output_State (Id : E) return B is
+   begin
+      return
+        Ekind (Id) = E_Abstract_State and then Has_Property (Id, Name_Output);
+   end Is_Output_State;
+
    -----------------------------------
    -- Is_Package_Or_Generic_Package --
    -----------------------------------
@@ -6376,33 +6486,6 @@ 
         Ekind (Id) = E_Generic_Package;
    end Is_Package_Or_Generic_Package;
 
-   ------------------------
-   -- Predicate_Function --
-   ------------------------
-
-   function Predicate_Function (Id : E) return E is
-      S : Entity_Id;
-
-   begin
-      pragma Assert (Is_Type (Id));
-
-      if No (Subprograms_For_Type (Id)) then
-         return Empty;
-
-      else
-         S := Subprograms_For_Type (Id);
-         while Present (S) loop
-            if Has_Predicates (S) then
-               return S;
-            else
-               S := Subprograms_For_Type (S);
-            end if;
-         end loop;
-
-         return Empty;
-      end if;
-   end Predicate_Function;
-
    ---------------
    -- Is_Prival --
    ---------------
@@ -6534,6 +6617,17 @@ 
           and then Is_Task_Type (Corresponding_Concurrent_Type (Id));
    end Is_Task_Record_Type;
 
+   -----------------------
+   -- Is_Volatile_State --
+   -----------------------
+
+   function Is_Volatile_State (Id : E) return B is
+   begin
+      return
+        Ekind (Id) = E_Abstract_State
+          and then Has_Property (Id, Name_Volatile);
+   end Is_Volatile_State;
+
    ------------------------
    -- Is_Wrapper_Package --
    ------------------------
@@ -6917,6 +7011,33 @@ 
       return Ekind (Id);
    end Parameter_Mode;
 
+   ------------------------
+   -- Predicate_Function --
+   ------------------------
+
+   function Predicate_Function (Id : E) return E is
+      S : Entity_Id;
+
+   begin
+      pragma Assert (Is_Type (Id));
+
+      if No (Subprograms_For_Type (Id)) then
+         return Empty;
+
+      else
+         S := Subprograms_For_Type (Id);
+         while Present (S) loop
+            if Has_Predicates (S) then
+               return S;
+            else
+               S := Subprograms_For_Type (S);
+            end if;
+         end loop;
+
+         return Empty;
+      end if;
+   end Predicate_Function;
+
    -------------------------
    -- Present_In_Rep_Item --
    -------------------------
@@ -7835,6 +7956,9 @@ 
          when E_Variable                                   =>
             Write_Str ("Hiding_Loop_Variable");
 
+         when E_Abstract_State                             =>
+            Write_Str ("Integrity_Level");
+
          when Formal_Kind                                  |
               E_Function                                   |
               E_Subprogram_Body                            =>
@@ -7868,6 +7992,9 @@ 
          when Object_Kind                                  =>
             Write_Str ("Current_Value");
 
+         when E_Abstract_State                             =>
+            Write_Str ("Refined_State");
+
          when E_Function                                   |
               E_Generic_Function                           |
               E_Generic_Package                            |
@@ -8594,6 +8721,9 @@ 
    procedure Write_Field25_Name (Id : Entity_Id) is
    begin
       case Ekind (Id) is
+         when E_Package                                    =>
+            Write_Str ("Abstract_States");
+
          when E_Variable                                   =>
             Write_Str ("Debug_Renaming_Link");
 
Index: einfo.ads
===================================================================
--- einfo.ads	(revision 194847)
+++ einfo.ads	(working copy)
@@ -327,6 +327,10 @@ 
 --  type, and if assertions are enabled, an attempt to set the attribute on a
 --  subtype will raise an assert error.
 
+--    Abstract_States (Elist25)
+--       Defined for E_Package entities. Contains a list of all the abstract
+--       states declared by the related package.
+
 --    Accept_Address (Elist21)
 --       Defined in entries. If an accept has a statement sequence, then an
 --       address variable is created, which is used to hold the address of the
@@ -1907,18 +1911,6 @@ 
 --       that we still have a concrete type. For entities other than types,
 --       returns the entity unchanged.
 
---    Interface_Alias (Node25)
---       Defined in subprograms that cover a primitive operation of an abstract
---       interface type. Can be set only if the Is_Hidden flag is also set,
---       since such entities are always hidden. Points to its associated
---       interface subprogram. It is used to register the subprogram in
---       secondary dispatch table of the interface (Ada 2005: AI-251).
-
---    Interfaces (Elist25)
---       Defined in record types and subtypes. List of abstract interfaces
---       implemented by a tagged type that are not already implemented by the
---       ancestors (Ada 2005: AI-251).
-
 --    In_Package_Body (Flag48)
 --       Defined in package entities. Set on the entity that denotes the
 --       package (the defining occurrence of the package declaration) while
@@ -1943,6 +1935,18 @@ 
 --       instantiated within the given generic. Used to diagnose circular
 --       instantiations.
 
+--    Integrity_Level (Uint8)
+--       Defined for E_Abstract_State entities. Contains the numerical value of
+--       the integrity level state property. A value of Uint_0 designates a non
+--       existent integrity.
+
+--    Interface_Alias (Node25)
+--       Defined in subprograms that cover a primitive operation of an abstract
+--       interface type. Can be set only if the Is_Hidden flag is also set,
+--       since such entities are always hidden. Points to its associated
+--       interface subprogram. It is used to register the subprogram in
+--       secondary dispatch table of the interface (Ada 2005: AI-251).
+
 --    Interface_Name (Node21)
 --       Defined in constants, variables, exceptions, functions, procedures,
 --       packages, components (JGNAT only), discriminants (JGNAT only), and
@@ -1967,6 +1971,11 @@ 
 --       External_Name of the imported Java field (which is generally needed,
 --       because Java names are case sensitive).
 
+--    Interfaces (Elist25)
+--       Defined in record types and subtypes. List of abstract interfaces
+--       implemented by a tagged type that are not already implemented by the
+--       ancestors (Ada 2005: AI-251).
+
 --    Invariant_Procedure (synthesized)
 --       Defined in types and subtypes. Set for private types if one or more
 --       Invariant, or Invariant'Class, or inherited Invariant'Class aspects
@@ -2329,6 +2338,10 @@ 
 --       inherited by their instances. It is also set on the body entities
 --       of inlined subprograms. See also Has_Pragma_Inline.
 
+--    Is_Input_State (synthesized)
+--       Applies to all entities, true for abstract states that are subject to
+--       property Input.
+
 --    Is_Instantiated (Flag126)
 --       Defined in generic packages and generic subprograms. Set if the unit
 --       is instantiated from somewhere in the extended main source unit. This
@@ -2523,6 +2536,10 @@ 
 --       but there is no need to call such procedures within a compilation
 --       unit, and this flag is used to suppress such calls.
 
+--    Is_Null_State (synthesized)
+--       Applies to all entities, true for an abstract state declared with
+--       keyword null.
+
 --    Is_Numeric_Type (synthesized)
 --       Applies to all entities, true for all numeric types and subtypes
 --       (integer, fixed, float).
@@ -2550,6 +2567,10 @@ 
 --       Applies to all entities, true for ordinary fixed point types and
 --       subtypes.
 
+--    Is_Output_State (synthesized)
+--       Applies to all entities, true for abstract states that are subject to
+--       property Output.
+
 --    Is_Package_Or_Generic_Package (synthesized)
 --       Applies to all entities. True for packages and generic packages.
 --       False for all other entities.
@@ -2895,6 +2916,10 @@ 
 --       optimizations on volatile objects should test Treat_As_Volatile
 --       rather than testing this flag.
 
+--    Is_Volatile_State (synthesized)
+--       Applies to all entities, true for abstract states that are subject to
+--       property Volatile.
+
 --    Is_Wrapper_Package (synthesized)
 --       Defined in package entities. Indicates that the package has been
 --       created as a wrapper for a subprogram instantiation.
@@ -3441,6 +3466,10 @@ 
 --       we have a separate warning for variables that are only assigned and
 --       never read, and out parameters are a special case.
 
+--    Refined_State (Node9)
+--       Defined in E_Abstract_State entities. Contains the entity of the
+--       abstract state completion which is usually foung in package bodies.
+
 --    Register_Exception_Call (Node20)
 --       Defined in exception entities. When an exception is declared,
 --       a call is expanded to Register_Exception. This field points to
@@ -4400,11 +4429,16 @@ 
       --  A task body. This entity serves almost no function, since all
       --  semantic analysis uses the protected entity (E_Task_Type).
 
-      E_Subprogram_Body
+      E_Subprogram_Body,
       --  A subprogram body. Used when a subprogram has a separate declaration
       --  to represent the entity for the body. This entity serves almost no
       --  function, since all semantic analysis uses the subprogram entity
       --  for the declaration (E_Function or E_Procedure).
+
+      E_Abstract_State
+      --  A state abstraction. Used to designate entities introduced by aspect
+      --  or pragma Abstract_State. The entity carries the various properties
+      --  of the state.
    );
 
    for Entity_Kind'Size use 8;
@@ -4972,6 +5006,14 @@ 
    -- Applicable attributes by entity kind --
    ------------------------------------------
 
+   --  E_Abstract_State
+   --    Integrity_Level                     (Uint8)
+   --    Refined_State                       (Node9)
+   --    Is_Input_State                      (synth)
+   --    Is_Null_State                       (synth)
+   --    Is_Output_State                     (synth)
+   --    Is_Volatile_State                   (synth)
+
    --  E_Access_Protected_Subprogram_Type
    --    Equivalent_Type                     (Node18)
    --    Directly_Designated_Type            (Node20)
@@ -5480,8 +5522,9 @@ 
    --    Inner_Instances                     (Elist23)  (generic case only)
    --    Limited_View                        (Node23)   (non-generic/instance)
    --    Finalizer                           (Node24)   (non-generic case only)
+   --    Abstract_States                     (Elist25)
+   --    Package_Instantiation               (Node26)
    --    Current_Use_Clause                  (Node27)
-   --    Package_Instantiation               (Node26)
    --    Delay_Subprogram_Descriptors        (Flag50)
    --    Body_Needed_For_SAL                 (Flag40)
    --    Discard_Names                       (Flag88)
@@ -6040,6 +6083,7 @@ 
    --  section contains the functions used to obtain attribute values which
    --  correspond to values in fields or flags in the entity itself.
 
+   function Abstract_States                     (Id : E) return L;
    function Accept_Address                      (Id : E) return L;
    function Access_Disp_Table                   (Id : E) return L;
    function Actual_Subtype                      (Id : E) return E;
@@ -6226,6 +6270,7 @@ 
    function In_Private_Part                     (Id : E) return B;
    function In_Use                              (Id : E) return B;
    function Initialization_Statements           (Id : E) return N;
+   function Integrity_Level                     (Id : E) return U;
    function Inner_Instances                     (Id : E) return L;
    function Interface_Alias                     (Id : E) return E;
    function Interface_Name                      (Id : E) return N;
@@ -6380,6 +6425,7 @@ 
    function Referenced                          (Id : E) return B;
    function Referenced_As_LHS                   (Id : E) return B;
    function Referenced_As_Out_Parameter         (Id : E) return B;
+   function Refined_State                       (Id : E) return E;
    function Register_Exception_Call             (Id : E) return N;
    function Related_Array_Object                (Id : E) return E;
    function Related_Expression                  (Id : E) return N;
@@ -6524,6 +6570,9 @@ 
    function Is_Discriminal                      (Id : E) return B;
    function Is_Dynamic_Scope                    (Id : E) return B;
    function Is_Finalizer                        (Id : E) return B;
+   function Is_Input_State                      (Id : E) return B;
+   function Is_Null_State                       (Id : E) return B;
+   function Is_Output_State                     (Id : E) return B;
    function Is_Package_Or_Generic_Package       (Id : E) return B;
    function Is_Prival                           (Id : E) return B;
    function Is_Protected_Component              (Id : E) return B;
@@ -6534,6 +6583,7 @@ 
    function Is_Synchronized_Interface           (Id : E) return B;
    function Is_Task_Interface                   (Id : E) return B;
    function Is_Task_Record_Type                 (Id : E) return B;
+   function Is_Volatile_State                   (Id : E) return B;
    function Is_Wrapper_Package                  (Id : E) return B;
    function Last_Formal                         (Id : E) return E;
    function Machine_Emax_Value                  (Id : E) return U;
@@ -6634,6 +6684,7 @@ 
    -- Attribute Set Procedures --
    ------------------------------
 
+   procedure Set_Abstract_States                 (Id : E; V : L);
    procedure Set_Accept_Address                  (Id : E; V : L);
    procedure Set_Access_Disp_Table               (Id : E; V : L);
    procedure Set_Actual_Subtype                  (Id : E; V : E);
@@ -6819,6 +6870,7 @@ 
    procedure Set_In_Private_Part                 (Id : E; V : B := True);
    procedure Set_In_Use                          (Id : E; V : B := True);
    procedure Set_Initialization_Statements       (Id : E; V : N);
+   procedure Set_Integrity_Level                 (Id : E; V : U);
    procedure Set_Inner_Instances                 (Id : E; V : L);
    procedure Set_Interface_Alias                 (Id : E; V : E);
    procedure Set_Interface_Name                  (Id : E; V : N);
@@ -6979,6 +7031,7 @@ 
    procedure Set_Referenced                      (Id : E; V : B := True);
    procedure Set_Referenced_As_LHS               (Id : E; V : B := True);
    procedure Set_Referenced_As_Out_Parameter     (Id : E; V : B := True);
+   procedure Set_Refined_State                   (Id : E; V : E);
    procedure Set_Register_Exception_Call         (Id : E; V : N);
    procedure Set_Related_Array_Object            (Id : E; V : E);
    procedure Set_Related_Expression              (Id : E; V : N);
@@ -7317,6 +7370,7 @@ 
    --  subprograms meeting the requirements documented in the section on
    --  XEINFO may be referenced in this section.
 
+   pragma Inline (Abstract_States);
    pragma Inline (Accept_Address);
    pragma Inline (Access_Disp_Table);
    pragma Inline (Actual_Subtype);
@@ -7499,6 +7553,7 @@ 
    pragma Inline (In_Package_Body);
    pragma Inline (In_Private_Part);
    pragma Inline (In_Use);
+   pragma Inline (Integrity_Level);
    pragma Inline (Inner_Instances);
    pragma Inline (Interface_Alias);
    pragma Inline (Interface_Name);
@@ -7702,6 +7757,7 @@ 
    pragma Inline (Referenced);
    pragma Inline (Referenced_As_LHS);
    pragma Inline (Referenced_As_Out_Parameter);
+   pragma Inline (Refined_State);
    pragma Inline (Register_Exception_Call);
    pragma Inline (Related_Array_Object);
    pragma Inline (Related_Expression);
@@ -7766,6 +7822,7 @@ 
    pragma Inline (Init_Esize);
    pragma Inline (Init_RM_Size);
 
+   pragma Inline (Set_Abstract_States);
    pragma Inline (Set_Accept_Address);
    pragma Inline (Set_Access_Disp_Table);
    pragma Inline (Set_Actual_Subtype);
@@ -7947,6 +8004,7 @@ 
    pragma Inline (Set_In_Private_Part);
    pragma Inline (Set_In_Use);
    pragma Inline (Set_Inner_Instances);
+   pragma Inline (Set_Integrity_Level);
    pragma Inline (Set_Interface_Alias);
    pragma Inline (Set_Interface_Name);
    pragma Inline (Set_Interfaces);
@@ -8106,6 +8164,7 @@ 
    pragma Inline (Set_Referenced);
    pragma Inline (Set_Referenced_As_LHS);
    pragma Inline (Set_Referenced_As_Out_Parameter);
+   pragma Inline (Set_Refined_State);
    pragma Inline (Set_Register_Exception_Call);
    pragma Inline (Set_Related_Array_Object);
    pragma Inline (Set_Related_Expression);
Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 194841)
+++ sem_prag.adb	(working copy)
@@ -6640,6 +6640,280 @@ 
                Pragma_Misplaced;
             end if;
 
+         --------------------
+         -- Abstract_State --
+         --------------------
+
+         when Pragma_Abstract_State => Abstract_State : declare
+            Pack_Id : Entity_Id;
+
+            --  Flags used to verify the consistency of states
+
+            Non_Null_Seen : Boolean := False;
+            Null_Seen     : Boolean := False;
+
+            procedure Analyze_Abstract_State (State : Node_Id);
+            --  Verify the legality of a single state declaration. Create and
+            --  decorate a state abstraction entity and introduce it into the
+            --  visibility chain.
+
+            ----------------------------
+            -- Analyze_Abstract_State --
+            ----------------------------
+
+            procedure Analyze_Abstract_State (State : Node_Id) is
+               procedure Check_Duplicate_Property
+                 (Prop   : Node_Id;
+                  Status : in out Boolean);
+               --  Flag Status denotes whether a particular property has been
+               --  seen while processing a state. This routine verifies that
+               --  Prop is not a duplicate property and sets the flag Status.
+
+               ------------------------------
+               -- Check_Duplicate_Property --
+               ------------------------------
+
+               procedure Check_Duplicate_Property
+                 (Prop   : Node_Id;
+                  Status : in out Boolean)
+               is
+               begin
+                  if Status then
+                     Error_Msg_N ("duplicate state property", Prop);
+                  end if;
+
+                  Status := True;
+               end Check_Duplicate_Property;
+
+               --  Local variables
+
+               Errors  : constant Nat := Serious_Errors_Detected;
+               Loc     : constant Source_Ptr := Sloc (State);
+               Assoc   : Node_Id;
+               Id      : Entity_Id;
+               Is_Null : Boolean := False;
+               Level   : Uint := Uint_0;
+               Name    : Name_Id;
+               Prop    : Node_Id;
+
+               --  Flags used to verify the consistency of properties
+
+               Input_Seen     : Boolean := False;
+               Integrity_Seen : Boolean := False;
+               Output_Seen    : Boolean := False;
+               Volatile_Seen  : Boolean := False;
+
+            --  Start of processing for Analyze_Abstract_State
+
+            begin
+               --  A package with a null abstract state is not allowed to
+               --  declare additional states.
+
+               if Null_Seen then
+                  Error_Msg_Name_1 := Chars (Pack_Id);
+                  Error_Msg_N ("package % has null abstract state", State);
+
+               --  Null states appear as internally generated entities
+
+               elsif Nkind (State) = N_Null then
+                  Name := New_Internal_Name ('S');
+                  Is_Null   := True;
+                  Null_Seen := True;
+
+                  --  Catch a case where a null state appears in a list of
+                  --  non-null states.
+
+                  if Non_Null_Seen then
+                     Error_Msg_Name_1 := Chars (Pack_Id);
+                     Error_Msg_N
+                       ("package % has non-null abstract state", State);
+                  end if;
+
+               --  Simple state declaration
+
+               elsif Nkind (State) = N_Identifier then
+                  Name := Chars (State);
+                  Non_Null_Seen := True;
+
+               --  State declaration with various properties. This construct
+               --  appears as an extension aggregate in the tree.
+
+               elsif Nkind (State) = N_Extension_Aggregate then
+                  if Nkind (Ancestor_Part (State)) = N_Identifier then
+                     Name := Chars (Ancestor_Part (State));
+                     Non_Null_Seen := True;
+                  else
+                     Error_Msg_N
+                       ("state name must be an identifier",
+                        Ancestor_Part (State));
+                  end if;
+
+                  --  Process properties Input, Output and Volatile. Ensure
+                  --  that none of them appear more than once.
+
+                  Prop := First (Expressions (State));
+                  while Present (Prop) loop
+                     if Nkind (Prop) = N_Identifier then
+                        if Chars (Prop) = Name_Input then
+                           Check_Duplicate_Property (Prop, Input_Seen);
+                        elsif Chars (Prop) = Name_Output then
+                           Check_Duplicate_Property (Prop, Output_Seen);
+                        elsif Chars (Prop) = Name_Volatile then
+                           Check_Duplicate_Property (Prop, Volatile_Seen);
+                        else
+                           Error_Msg_N ("invalid state property", Prop);
+                        end if;
+                     else
+                        Error_Msg_N ("invalid state property", Prop);
+                     end if;
+
+                     Next (Prop);
+                  end loop;
+
+                  --  Volatile requires exactly one Input or Output
+
+                  if Volatile_Seen
+                    and then
+                      ((Input_Seen and then Output_Seen)           --  both
+                          or else
+                       (not Input_Seen and then not Output_Seen))  --  none
+                  then
+                     Error_Msg_N
+                       ("property Volatile requires exactly one Input or " &
+                        "Output", State);
+                  end if;
+
+                  --  Either Input or Output require Volatile
+
+                  if (Input_Seen or else Output_Seen)
+                    and then not Volatile_Seen
+                  then
+                     Error_Msg_N
+                       ("properties Input and Output require Volatile", State);
+                  end if;
+
+                  --  State property Integrity appears as a component
+                  --  association.
+
+                  Assoc := First (Component_Associations (State));
+                  while Present (Assoc) loop
+                     Prop := First (Choices (Assoc));
+                     while Present (Prop) loop
+                        if Nkind (Prop) = N_Identifier
+                          and then Chars (Prop) = Name_Integrity
+                        then
+                           Check_Duplicate_Property (Prop, Integrity_Seen);
+                        else
+                           Error_Msg_N ("invalid state property", Prop);
+                        end if;
+
+                        Next (Prop);
+                     end loop;
+
+                     if Nkind (Expression (Assoc)) = N_Integer_Literal then
+                        Level := Intval (Expression (Assoc));
+                     else
+                        Error_Msg_N
+                          ("integrity level must be an integer literal",
+                           Expression (Assoc));
+                     end if;
+
+                     Next (Assoc);
+                  end loop;
+
+               --  Any other attempt to declare a state is erroneous
+
+               else
+                  Error_Msg_N ("malformed abstract state declaration", N);
+               end if;
+
+               --  Do not generate a state abstraction entity if it was not
+               --  properly declared.
+
+               if Serious_Errors_Detected > Errors then
+                  return;
+               end if;
+
+               --  The generated state abstraction reuses the same characters
+               --  from the original state declaration. Decorate the entity.
+
+               Id := Make_Defining_Identifier (Loc, New_External_Name (Name));
+               Set_Comes_From_Source (Id, not Is_Null);
+               Set_Parent            (Id, State);
+               Set_Ekind             (Id, E_Abstract_State);
+               Set_Etype             (Id, Standard_Void_Type);
+               Set_Integrity_Level   (Id, Level);
+               Set_Refined_State     (Id, Empty);
+
+               --  Every non-null state must be nameable and resolvable the
+               --  same way a constant is.
+
+               if not Is_Null then
+                  Push_Scope (Pack_Id);
+                  Enter_Name (Id);
+                  Pop_Scope;
+               end if;
+
+               --  Associate the state with its related package
+
+               if No (Abstract_States (Pack_Id)) then
+                  Set_Abstract_States (Pack_Id, New_Elmt_List);
+               end if;
+
+               Append_Elmt (Id, Abstract_States (Pack_Id));
+            end Analyze_Abstract_State;
+
+            --  Local variables
+
+            Par   : Node_Id;
+            State : Node_Id;
+
+         --  Start of processing for Abstract_State
+
+         begin
+            GNAT_Pragma;
+            S14_Pragma;
+            Check_Arg_Count (1);
+
+            --  Ensure the proper placement of the pragma. Abstract states must
+            --  be associated with a package declaration.
+
+            if From_Aspect_Specification (N) then
+               Par := Parent (Corresponding_Aspect (N));
+            else
+               Par := Parent (Parent (N));
+            end if;
+
+            if Nkind (Par) = N_Compilation_Unit then
+               Par := Unit (Par);
+            end if;
+
+            if Nkind (Par) /= N_Package_Declaration then
+               Pragma_Misplaced;
+               return;
+            end if;
+
+            Pack_Id := Defining_Unit_Name (Specification (Par));
+            State   := Expression (Arg1);
+
+            --  Multiple abstract states appear as an aggregate
+
+            if Nkind (State) = N_Aggregate then
+               State := First (Expressions (State));
+               while Present (State) loop
+                  Analyze_Abstract_State (State);
+
+                  Next (State);
+               end loop;
+
+            --  Various forms of a single abstract state. Note that these may
+            --  include malformed state declarations.
+
+            else
+               Analyze_Abstract_State (State);
+            end if;
+         end Abstract_State;
+
          ------------
          -- Ada_83 --
          ------------
@@ -15748,6 +16022,7 @@ 
    Sig_Flags : constant array (Pragma_Id) of Int :=
      (Pragma_AST_Entry                      => -1,
       Pragma_Abort_Defer                    => -1,
+      Pragma_Abstract_State                 => -1,
       Pragma_Ada_83                         => -1,
       Pragma_Ada_95                         => -1,
       Pragma_Ada_05                         => -1,
Index: aspects.adb
===================================================================
--- aspects.adb	(revision 194841)
+++ aspects.adb	(working copy)
@@ -238,6 +238,7 @@ 
 
    Canonical_Aspect : constant array (Aspect_Id) of Aspect_Id :=
    (No_Aspect                           => No_Aspect,
+    Aspect_Abstract_State               => Aspect_Abstract_State,
     Aspect_Ada_2005                     => Aspect_Ada_2005,
     Aspect_Ada_2012                     => Aspect_Ada_2005,
     Aspect_Address                      => Aspect_Address,
Index: aspects.ads
===================================================================
--- aspects.ads	(revision 194841)
+++ aspects.ads	(working copy)
@@ -74,6 +74,7 @@ 
 
    type Aspect_Id is
      (No_Aspect,                            -- Dummy entry for no aspect
+      Aspect_Abstract_State,                -- GNAT
       Aspect_Address,
       Aspect_Alignment,
       Aspect_Attach_Handler,
@@ -221,7 +222,8 @@ 
    --  The following array identifies all implementation defined aspects
 
    Impl_Defined_Aspects : constant array (Aspect_Id) of Boolean :=
-                            (Aspect_Ada_2005                 => True,
+                            (Aspect_Abstract_State           => True,
+                             Aspect_Ada_2005                 => True,
                              Aspect_Ada_2012                 => True,
                              Aspect_Compiler_Unit            => True,
                              Aspect_Contract_Case            => True,
@@ -305,6 +307,7 @@ 
 
    Aspect_Argument : constant array (Aspect_Id) of Aspect_Expression :=
                        (No_Aspect                      => Optional,
+                        Aspect_Abstract_State          => Expression,
                         Aspect_Address                 => Expression,
                         Aspect_Alignment               => Expression,
                         Aspect_Attach_Handler          => Expression,
@@ -370,6 +373,7 @@ 
 
    Aspect_Names : constant array (Aspect_Id) of Name_Id := (
      No_Aspect                           => No_Name,
+     Aspect_Abstract_State               => Name_Abstract_State,
      Aspect_Ada_2005                     => Name_Ada_2005,
      Aspect_Ada_2012                     => Name_Ada_2012,
      Aspect_Address                      => Name_Address,
Index: par-prag.adb
===================================================================
--- par-prag.adb	(revision 194841)
+++ par-prag.adb	(working copy)
@@ -1092,6 +1092,7 @@ 
       --  entirely in Sem_Prag, and no further checking is done by Par.
 
       when Pragma_Abort_Defer                    |
+           Pragma_Abstract_State                 |
            Pragma_Assertion_Policy               |
            Pragma_Assume                         |
            Pragma_Assume_No_Invalid_Values       |
Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb	(revision 194849)
+++ sem_ch13.adb	(working copy)
@@ -1434,13 +1434,23 @@ 
                --  Case 2d : Aspects that correspond to a pragma with one
                --  argument.
 
+               when Aspect_Abstract_State        =>
+                  Aitem :=
+                    Make_Pragma (Loc,
+                      Pragma_Identifier            =>
+                        Make_Identifier (Sloc (Id), Name_Abstract_State),
+                      Pragma_Argument_Associations => New_List (
+                        Make_Pragma_Argument_Association (Loc,
+                          Expression => Relocate_Node (Expr))));
+
+                  Delay_Required := False;
+
                when Aspect_Relative_Deadline     =>
                   Aitem :=
                     Make_Pragma (Loc,
-                      Pragma_Argument_Associations =>
-                        New_List (
-                          Make_Pragma_Argument_Association (Loc,
-                             Expression => Relocate_Node (Expr))),
+                      Pragma_Argument_Associations => New_List (
+                        Make_Pragma_Argument_Association (Loc,
+                          Expression => Relocate_Node (Expr))),
                       Pragma_Identifier            =>
                         Make_Identifier (Sloc (Id), Name_Relative_Deadline));
 
@@ -6961,9 +6971,10 @@ 
               Aspect_Type_Invariant    =>
             T := Standard_Boolean;
 
-         --  Here is the list of aspects that don't require delay analysis.
+         --  Here is the list of aspects that don't require delay analysis
 
-         when Aspect_Contract_Case        |
+         when Aspect_Abstract_State       |
+              Aspect_Contract_Case        |
               Aspect_Contract_Cases       |
               Aspect_Dimension            |
               Aspect_Dimension_System     |
Index: snames.ads-tmpl
===================================================================
--- snames.ads-tmpl	(revision 194841)
+++ snames.ads-tmpl	(working copy)
@@ -446,6 +446,7 @@ 
    --  Remaining pragma names
 
    Name_Abort_Defer                    : constant Name_Id := N + $; -- GNAT
+   Name_Abstract_State                 : constant Name_Id := N + $; -- GNAT
    Name_All_Calls_Remote               : constant Name_Id := N + $;
 
    --  Note: AST_Entry is not in this list because its name matches the name of
@@ -696,6 +697,7 @@ 
    Name_Ignore                         : constant Name_Id := N + $;
    Name_Increases                      : constant Name_Id := N + $;
    Name_Info                           : constant Name_Id := N + $;
+   Name_Integrity                      : constant Name_Id := N + $;
    Name_Internal                       : constant Name_Id := N + $;
    Name_Link_Name                      : constant Name_Id := N + $;
    Name_Lowercase                      : constant Name_Id := N + $;
@@ -1731,6 +1733,7 @@ 
       --  Remaining (non-configuration) pragmas
 
       Pragma_Abort_Defer,
+      Pragma_Abstract_State,
       Pragma_All_Calls_Remote,
       Pragma_Assert,
       Pragma_Assert_And_Cut,
Index: lib-xref.ads
===================================================================
--- lib-xref.ads	(revision 194841)
+++ lib-xref.ads	(working copy)
@@ -531,8 +531,13 @@ 
       E_Protected_Object                           => ' ',
       E_Protected_Body                             => ' ',
       E_Task_Body                                  => ' ',
-      E_Subprogram_Body                            => ' ');
+      E_Subprogram_Body                            => ' ',
 
+      --  ??? The following letter is added for completion, proper design and
+      --  implementation of abstract state cross-referencing to follow.
+
+      E_Abstract_State                             => ' ');
+
    --  The following table is for information purposes. It shows the use of
    --  each character appearing as an entity type.