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.