[multiple changes]

2013-10-10  Hristian Kirtchev  <kirtchev@adacore.com>

	* einfo.adb: Remove Integrity_Level from the node usage list.
	(Has_Option): Update the implementation to match
	the new terminology.
	(Has_Property): Renamed to Has_Option.
	(Integrity_Level): Removed.
	(Is_External_State): New routine.
	(Is_Input_Only_State): Use Has_Option to determine whether a state
	is Input_Only.	(Is_Input_State): Renamed to Is_Input_Only_State.
	(Is_Output_Only_State): Use Has_Option to determine whether
	a state is Output_Only.
	(Is_Output_State): Renamed to
	Is_Output_Only_State.
	(Is_Volatile_State): Use Has_Option to determine whether a state is
	volatile.
	(Set_Integrity_Level): Removed.
	(Write_Field8): Remove the entry for Integrity_Level.
	* einfo.ads: Remove Integrity_Level along with its documentation
	and usage in nodes.  Rename Is_Input_State to Is_Input_Only_State.
	Rename Is_Output_State to Is_Output_Only_State.  Update the
	documentation of Is_Volatile_State.  Update the node structure of
	E_Abstract_Entity.
	(Integrity_Level): Removed along with pragma Inline.
	(Is_External_State): New routine.
	(Is_Input_State): Renamed to Is_Input_Only_State.
	(Is_Output_State): Renamed to Is_Output_Only_State.
	(Set_Integrity_Level): Removed along with pragma Inline.
	* sem_prag.adb (Analyze_Pragma): Update the checks regarding
	global items and abstract state modes. Update the implementation
	of pragma Abstract_State to reflect the new rules and terminology.
	* snames.ads-tmpl: Remove the predefined name for Integrity
	level. Add new predefined names for Input_Only, Non_Volatile,
	Output_Only and Part_Of.

2013-10-10  Ed Schonberg  <schonberg@adacore.com>

	* lib-xref.adb (Generate_Reference): Do not generate a reference
	within a _postcondition procedure: a proper source reference has
	already been generated when pre- analyzing the original aspect
	specification, and the use of a formal in a pre/postcondition
	should not count as a proper use in a subprogram body.

2013-10-10  Robert Dewar  <dewar@adacore.com>

	* sem_eval.adb (Why_Non_Static): Fix bomb for deferred constant
	case

From-SVN: r203360

gcc/ada/ChangeLog

 2013-10-10  Hristian Kirtchev  <kirtchev@adacore.com>
 
+	* einfo.adb: Remove Integrity_Level from the node usage list.
+	(Has_Option): Update the implementation to match
+	the new terminology.
+	(Has_Property): Renamed to Has_Option.
+	(Integrity_Level): Removed.
+	(Is_External_State): New routine.
+	(Is_Input_Only_State): Use Has_Option to determine whether a state
+	is Input_Only.	(Is_Input_State): Renamed to Is_Input_Only_State.
+	(Is_Output_Only_State): Use Has_Option to determine whether
+	a state is Output_Only.
+	(Is_Output_State): Renamed to
+	Is_Output_Only_State.
+	(Is_Volatile_State): Use Has_Option to determine whether a state is
+	volatile.
+	(Set_Integrity_Level): Removed.
+	(Write_Field8): Remove the entry for Integrity_Level.
+	* einfo.ads: Remove Integrity_Level along with its documentation
+	and usage in nodes.  Rename Is_Input_State to Is_Input_Only_State.
+	Rename Is_Output_State to Is_Output_Only_State.  Update the
+	documentation of Is_Volatile_State.  Update the node structure of
+	E_Abstract_Entity.
+	(Integrity_Level): Removed along with pragma Inline.
+	(Is_External_State): New routine.
+	(Is_Input_State): Renamed to Is_Input_Only_State.
+	(Is_Output_State): Renamed to Is_Output_Only_State.
+	(Set_Integrity_Level): Removed along with pragma Inline.
+	* sem_prag.adb (Analyze_Pragma): Update the checks regarding
+	global items and abstract state modes. Update the implementation
+	of pragma Abstract_State to reflect the new rules and terminology.
+	* snames.ads-tmpl: Remove the predefined name for Integrity
+	level. Add new predefined names for Input_Only, Non_Volatile,
+	Output_Only and Part_Of.
+
+2013-10-10  Ed Schonberg  <schonberg@adacore.com>
+
+	* lib-xref.adb (Generate_Reference): Do not generate a reference
+	within a _postcondition procedure: a proper source reference has
+	already been generated when pre- analyzing the original aspect
+	specification, and the use of a formal in a pre/postcondition
+	should not count as a proper use in a subprogram body.
+
+2013-10-10  Robert Dewar  <dewar@adacore.com>
+
+	* sem_eval.adb (Why_Non_Static): Fix bomb for deferred constant
+	case
+
+2013-10-10  Hristian Kirtchev  <kirtchev@adacore.com>
+
 	* aspects.adb: Add an entry for Aspect_Refined_Post in table
 	Canonical_Aspect.
 	* aspects.ads: Add an entry for Aspect_Refined_Post in tables

gcc/ada/einfo.adb

@@ -76,7 +76,6 @@ package body Einfo is
    --    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
@@ -584,11 +583,11 @@ package body Einfo is
    -- 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 Has_Option
+     (State   : Entity_Id;
+      Opt_Nam : Name_Id) return Boolean;
+   --  Determine whether abstract state State has a particular option denoted
+   --  by the name Opt_Nam.
 
    ---------------
    -- Float_Rep --
@@ -600,40 +599,40 @@ package body Einfo is
       return F'Val (UI_To_Int (Uint10 (Base_Type (Id))));
    end Float_Rep;
 
-   ------------------
-   -- Has_Property --
-   ------------------
+   ----------------
+   -- Has_Option --
+   ----------------
 
-   function Has_Property
-     (State    : Entity_Id;
-      Prop_Nam : Name_Id) return Boolean
+   function Has_Option
+     (State   : Entity_Id;
+      Opt_Nam : Name_Id) return Boolean
    is
-      Par  : constant Node_Id := Parent (State);
-      Prop : Node_Id;
+      Par : constant Node_Id := Parent (State);
+      Opt : Node_Id;
 
    begin
       pragma Assert (Ekind (State) = E_Abstract_State);
 
-      --  States with properties appear as extension aggregates in the tree
+      --  States with options appear as extension aggregates in the tree
 
       if Nkind (Par) = N_Extension_Aggregate then
-         if Prop_Nam = Name_Integrity then
+         if Opt_Nam = Name_Part_Of then
             return Present (Component_Associations (Par));
 
          else
-            Prop := First (Expressions (Par));
-            while Present (Prop) loop
-               if Chars (Prop) = Prop_Nam then
+            Opt := First (Expressions (Par));
+            while Present (Opt) loop
+               if Chars (Opt) = Opt_Nam then
                   return True;
                end if;
 
-               Next (Prop);
+               Next (Opt);
             end loop;
          end if;
       end if;
 
       return False;
-   end Has_Property;
+   end Has_Option;
 
    --------------------------------
    -- Attribute Access Functions --
@@ -1760,12 +1759,6 @@ package body Einfo is
       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);
@@ -4386,12 +4379,6 @@ package body Einfo is
       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);
@@ -6655,6 +6642,16 @@ package body Einfo is
                   and then Is_Entity_Attribute_Name (Attribute_Name (N)));
    end Is_Entity_Name;
 
+   -----------------------
+   -- Is_External_State --
+   -----------------------
+
+   function Is_External_State (Id : E) return B is
+   begin
+      return
+        Ekind (Id) = E_Abstract_State and then Has_Option (Id, Name_External);
+   end Is_External_State;
+
    ------------------
    -- Is_Finalizer --
    ------------------
@@ -6690,15 +6687,16 @@ package body Einfo is
       end if;
    end Is_Ghost_Subprogram;
 
-   --------------------
-   -- Is_Input_State --
-   --------------------
+   -------------------------
+   -- Is_Input_Only_State --
+   -------------------------
 
-   function Is_Input_State (Id : E) return B is
+   function Is_Input_Only_State (Id : E) return B is
    begin
       return
-        Ekind (Id) = E_Abstract_State and then Has_Property (Id, Name_Input);
-   end Is_Input_State;
+        Ekind (Id) = E_Abstract_State
+          and then Has_Option (Id, Name_Input_Only);
+   end Is_Input_Only_State;
 
    -------------------
    -- Is_Null_State --
@@ -6714,11 +6712,12 @@ package body Einfo is
    -- Is_Output_State --
    ---------------------
 
-   function Is_Output_State (Id : E) return B is
+   function Is_Output_Only_State (Id : E) return B is
    begin
       return
-        Ekind (Id) = E_Abstract_State and then Has_Property (Id, Name_Output);
-   end Is_Output_State;
+        Ekind (Id) = E_Abstract_State
+          and then Has_Option (Id, Name_Output_Only);
+   end Is_Output_Only_State;
 
    -----------------------------------
    -- Is_Package_Or_Generic_Package --
@@ -6867,7 +6866,7 @@ package body Einfo is
    begin
       return
         Ekind (Id) = E_Abstract_State
-          and then Has_Property (Id, Name_Volatile);
+          and then Has_Option (Id, Name_Volatile);
    end Is_Volatile_State;
 
    ------------------------
@@ -8281,9 +8280,6 @@ package body Einfo is
          when E_Variable                                   =>
             Write_Str ("Hiding_Loop_Variable");
 
-         when E_Abstract_State                             =>
-            Write_Str ("Integrity_Level");
-
          when Formal_Kind                                  |
               E_Function                                   |
               E_Subprogram_Body                            =>

gcc/ada/einfo.ads

@@ -1969,11 +1969,6 @@ package Einfo is
 --       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,
@@ -2263,6 +2258,10 @@ package Einfo is
 --       and variables, but that may well change later on. Exceptions can only
 --       be exported in the OpenVMS and Java VM implementations of GNAT.
 
+--    Is_External_State (synthesized)
+--       Applies to all entities, true for abstract states that are subject to
+--       option External.
+
 --    Is_Finalizer (synthesized)
 --       Applies to all entities, true for procedures containing finalization
 --       code to process local or library level objects.
@@ -2380,9 +2379,9 @@ package Einfo is
 --       inherited by their instances. It is also set on the body entities
 --       of inlined subprograms. See also Has_Pragma_Inline.
 
---    Is_Input_State (synthesized)
+--    Is_Input_Only_State (synthesized)
 --       Applies to all entities, true for abstract states that are subject to
---       property Input.
+--       option Input_Only.
 
 --    Is_Instantiated (Flag126)
 --       Defined in generic packages and generic subprograms. Set if the unit
@@ -2613,9 +2612,9 @@ package Einfo is
 --       Applies to all entities, true for ordinary fixed point types and
 --       subtypes.
 
---    Is_Output_State (synthesized)
+--    Is_Output_Only_State (synthesized)
 --       Applies to all entities, true for abstract states that are subject to
---       property Output.
+--       option Output_Only.
 
 --    Is_Package_Or_Generic_Package (synthesized)
 --       Applies to all entities. True for packages and generic packages.
@@ -2976,7 +2975,7 @@ package Einfo is
 
 --    Is_Volatile_State (synthesized)
 --       Applies to all entities, true for abstract states that are subject to
---       property Volatile.
+--       option Volatile.
 
 --    Is_Wrapper_Package (synthesized)
 --       Defined in package entities. Indicates that the package has been
@@ -5093,11 +5092,11 @@ package Einfo is
    ------------------------------------------
 
    --  E_Abstract_State
-   --    Integrity_Level                     (Uint8)
    --    Refined_State                       (Node9)
-   --    Is_Input_State                      (synth)
+   --    Is_External_State                   (synth)
+   --    Is_Input_Only_State                 (synth)
    --    Is_Null_State                       (synth)
-   --    Is_Output_State                     (synth)
+   --    Is_Output_Only_State                (synth)
    --    Is_Volatile_State                   (synth)
 
    --  E_Access_Protected_Subprogram_Type
@@ -6377,7 +6376,6 @@ package Einfo is
    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;
@@ -6680,12 +6678,13 @@ package Einfo is
    function Is_Constant_Object                  (Id : E) return B;
    function Is_Discriminal                      (Id : E) return B;
    function Is_Dynamic_Scope                    (Id : E) return B;
+   function Is_External_State                   (Id : E) return B;
    function Is_Finalizer                        (Id : E) return B;
    function Is_Ghost_Entity                     (Id : E) return B;
    function Is_Ghost_Subprogram                 (Id : E) return B;
-   function Is_Input_State                      (Id : E) return B;
+   function Is_Input_Only_State                 (Id : E) return B;
    function Is_Null_State                       (Id : E) return B;
-   function Is_Output_State                     (Id : E) return B;
+   function Is_Output_Only_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;
@@ -6988,7 +6987,6 @@ package Einfo is
    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);
@@ -7696,7 +7694,6 @@ package Einfo is
    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);
@@ -8157,7 +8154,6 @@ package Einfo is
    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);

gcc/ada/lib-xref.adb

@@ -610,6 +610,15 @@ package body Lib.Xref is
          Error_Msg_NE ("& is only defined in Ada 2012?y?", N, E);
       end if;
 
+      --  Do not generate references if we are within a postcondition sub-
+      --  program, because the reference does not comes from source, and the
+      --  pre-analysis of the aspect has already created an entry for the ali
+      --  file at the proper source location.
+
+      if Chars (Current_Scope) = Name_uPostconditions then
+         return;
+      end if;
+
       --  Never collect references if not in main source unit. However, we omit
       --  this test if Typ is 'e' or 'k', since these entries are structural,
       --  and it is useful to have them in units that reference packages as

gcc/ada/sem_eval.adb

@@ -5578,7 +5578,7 @@ package body Sem_Eval is
                   then
                      Error_Msg_N ("\aggregate (#) is never static", N);
 
-                  elsif not Is_Static_Expression (CV) then
+                  elsif No (CV) or else not Is_Static_Expression (CV) then
                      Error_Msg_NE
                        ("\& is not a static constant (RM 4.9(5))", N, E);
                   end if;

gcc/ada/snames.ads-tmpl

@@ -713,7 +713,7 @@ package Snames is
    Name_In_Out                         : constant Name_Id := N + $;
    Name_Increases                      : constant Name_Id := N + $;
    Name_Info                           : constant Name_Id := N + $;
-   Name_Integrity                      : constant Name_Id := N + $;
+   Name_Input_Only                     : constant Name_Id := N + $;
    Name_Internal                       : constant Name_Id := N + $;
    Name_Link_Name                      : constant Name_Id := N + $;
    Name_Lowercase                      : constant Name_Id := N + $;
@@ -747,10 +747,13 @@ package Snames is
    Name_No_Unroll                      : constant Name_Id := N + $;
    Name_No_Vector                      : constant Name_Id := N + $;
    Name_Nominal                        : constant Name_Id := N + $;
+   Name_Non_Volatile                   : constant Name_Id := N + $;
    Name_On                             : constant Name_Id := N + $;
    Name_Optional                       : constant Name_Id := N + $;
+   Name_Output_Only                    : constant Name_Id := N + $;
    Name_Policy                         : constant Name_Id := N + $;
    Name_Parameter_Types                : constant Name_Id := N + $;
+   Name_Part_Of                        : constant Name_Id := N + $;
    Name_Reason                         : constant Name_Id := N + $;
    Name_Reference                      : constant Name_Id := N + $;
    Name_Requires                       : constant Name_Id := N + $;