[multiple changes]

2014-01-20  Hristian Kirtchev  <kirtchev@adacore.com>

	* einfo.ads: E_Abstract_State is now part of the entities that
	can be overloaded. Update type Overloadable_Kind to reflect the
	inclusion of abstract states.
	* sem_ch6.adb (New_Overloaded_Entity): A function can now
	overload an abstract state.
	* sem_prag.adb (Analyze_Constituent): Handle the overloading
	of states by functions. Use Entity_Of to obtain the entity of
	a constituent.	(Analyze_Global_Item): Handle the overloading of
	states by functions.
	(Analyze_Initialization_Item): Handle the
	overloading of states by functions.  Use Entity_Of to obtain the
	entity of an item.
	(Analyze_Input_Item): Handle the overloading
	of states by functions. Use Entity_Of to obtain the entity of an item.
	(Analyze_Input_Output): Handle the overloading of states by functions.
	(Analyze_Refinement_Clause): Handle the overloading
	of states by functions.  Use Entity_Of to obtain the entity of an item.
	(Appears_In): Use Entity_Of to obtain the entity of an element.
	(Check_Usage): Use Entity_Of to obtain the entity of
	an item. Add a guard to prevent a crash due to a previous error.
	(Resolve_State): New routine.

2014-01-20  Yannick Moy  <moy@adacore.com>

	* spark_xrefs.ads, debug.adb, gnat1drv.adb, errout.adb, errout.ads,
	opt.ads: Minor comments updates.

From-SVN: r206809

10 files changed, 132 insertions, 40 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 3eb79d6..d507793 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,5 +1,34 @@
 2014-01-20  Hristian Kirtchev  <kirtchev@adacore.com>
 
+	* einfo.ads: E_Abstract_State is now part of the entities that
+	can be overloaded. Update type Overloadable_Kind to reflect the
+	inclusion of abstract states.
+	* sem_ch6.adb (New_Overloaded_Entity): A function can now
+	overload an abstract state.
+	* sem_prag.adb (Analyze_Constituent): Handle the overloading
+	of states by functions. Use Entity_Of to obtain the entity of
+	a constituent.	(Analyze_Global_Item): Handle the overloading of
+	states by functions.
+	(Analyze_Initialization_Item): Handle the
+	overloading of states by functions.  Use Entity_Of to obtain the
+	entity of an item.
+	(Analyze_Input_Item): Handle the overloading
+	of states by functions. Use Entity_Of to obtain the entity of an item.
+	(Analyze_Input_Output): Handle the overloading of states by functions.
+	(Analyze_Refinement_Clause): Handle the overloading
+	of states by functions.  Use Entity_Of to obtain the entity of an item.
+	(Appears_In): Use Entity_Of to obtain the entity of an element.
+	(Check_Usage): Use Entity_Of to obtain the entity of
+	an item. Add a guard to prevent a crash due to a previous error.
+	(Resolve_State): New routine.
+
+2014-01-20  Yannick Moy  <moy@adacore.com>
+
+	* spark_xrefs.ads, debug.adb, gnat1drv.adb, errout.adb, errout.ads,
+	opt.ads: Minor comments updates.
+
+2014-01-20  Hristian Kirtchev  <kirtchev@adacore.com>
+
 	* einfo.adb (Non_Limited_View): Applies to abstract states.
 	(Set_From_Limited_With): Applies to abstract states.
 	(Set_Non_Limited_View): Applies to abstract states.
diff --git a/gcc/ada/debug.adb b/gcc/ada/debug.adb
index acda7cf..bb98c5c 100644
--- a/gcc/ada/debug.adb
+++ b/gcc/ada/debug.adb
@@ -606,9 +606,9 @@ package body Debug is
    --       ALI files to compute effects of subprograms. Note that ALI files
    --       are only written when option d.G is also given.
 
-   --  d.G  Frame condition mode for gnat2why. In this mode, gnat2why will not
-   --       generate Why code. Instead, it generates ALI files with an extra
-   --       section which contains the effects of subprograms.
+   --  d.G  Frame condition mode for gnat2why. In this mode, gnat2why will
+   --       generate ALI files with an extra section which contains the effects
+   --       of subprograms.
 
    --  d.I  Do not ignore enum representation clauses in CodePeer mode.
    --       The default of ignoring representation clauses for enumeration
diff --git a/gcc/ada/einfo.ads b/gcc/ada/einfo.ads
index ba6adc6..59ab153 100644
--- a/gcc/ada/einfo.ads
+++ b/gcc/ada/einfo.ads
@@ -4462,6 +4462,11 @@ package Einfo is
       --  An entry, created by an entry declaration in a task or protected
       --  object.
 
+      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.
+
       --------------------
       -- Other Entities --
       --------------------
@@ -4533,16 +4538,11 @@ package Einfo is
       --  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;
@@ -4792,7 +4792,8 @@ package Einfo is
    --  E_Function
    --  E_Operator
    --  E_Procedure
-       E_Entry;
+   --  E_Entry
+       E_Abstract_State;
 
    subtype Private_Kind                is Entity_Kind range
        E_Record_Type_With_Private ..
diff --git a/gcc/ada/errout.adb b/gcc/ada/errout.adb
index ab4dcfe..0e69062 100644
--- a/gcc/ada/errout.adb
+++ b/gcc/ada/errout.adb
@@ -234,7 +234,7 @@ package body Errout is
       if not Finalize_Called then
          raise Program_Error;
 
-      --  In formal verification mode, errors issued when generating Why code
+      --  In formal verification mode, errors issued when analyzing code
       --  are not compilation errors, and should not result in exiting with
       --  an error status. These errors are handled in the driver of the
       --  verification process instead.
diff --git a/gcc/ada/errout.ads b/gcc/ada/errout.ads
index e268d1f..0561329 100644
--- a/gcc/ada/errout.ads
+++ b/gcc/ada/errout.ads
@@ -818,7 +818,7 @@ package Errout is
    --  Returns True if errors have been detected, or warnings in -gnatwe (treat
    --  warnings as errors) mode. Note that it is mandatory to call Finalize
    --  before calling this routine. Always returns False in formal verification
-   --  mode, because errors issued when generating Why code are not compilation
+   --  mode, because errors issued when analyzing code are not compilation
    --  errors, and should not result in exiting with an error status.
 
    procedure Error_Msg_CRT (Feature : String; N : Node_Id);
diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb
index f1bc2f8..8693fd1 100644
--- a/gcc/ada/gnat1drv.adb
+++ b/gcc/ada/gnat1drv.adb
@@ -317,10 +317,10 @@ procedure Gnat1drv is
          end if;
 
          --  Distinguish between the two modes of gnat2why: frame condition
-         --  generation (generation of ALI files) and translation of Why (no
-         --  ALI files generated). This is done with the switch -gnatd.G,
-         --  which activates frame condition mode. The other changes in
-         --  behavior depending on this switch are done in gnat2why directly.
+         --  generation (generation of ALI files) and analysis (no ALI files
+         --  generated). This is done with the switch -gnatd.G, which activates
+         --  frame condition mode. The other changes in behavior depending on
+         --  this switch are done in gnat2why directly.
 
          if Debug_Flag_Dot_GG then
             Frame_Condition_Mode := True;
@@ -1057,7 +1057,7 @@ begin
       --  It is not an error to analyze in GNATprove mode a spec which requires
       --  a body, when the body is not available. During frame condition
       --  generation, the corresponding ALI file is generated. During
-      --  translation to Why, Why code is generated for the spec.
+      --  analysis, the spec is analyzed.
 
       elsif GNATprove_Mode then
          Back_End_Mode := Declarations_Only;
diff --git a/gcc/ada/opt.ads b/gcc/ada/opt.ads
index 2365abd..e06cf1e 100644
--- a/gcc/ada/opt.ads
+++ b/gcc/ada/opt.ads
@@ -1995,8 +1995,8 @@ package Opt is
    Frame_Condition_Mode : Boolean := False;
    --  Specific mode to be used in combination with GNATprove_Mode. If set to
    --  true, ALI files containing the frame conditions (global effects) are
-   --  generated, and Why files are *not* generated. If not true, Why files
-   --  are generated. Set by debug flag -gnatd.G.
+   --  generated, and analysis is *not* performed. If not true, analysis is
+   --  performed. Set by debug flag -gnatd.G.
 
    Formal_Extensions : Boolean := False;
    --  When this flag is set, new aspects/pragmas/attributes are accepted,
@@ -2008,12 +2008,11 @@ package Opt is
    --  in a configuration file such as gnat.adc.
 
    GNATprove_Mode : Boolean := False;
-   --  Specific compiling mode targeting formal verification through the
-   --  generation of Why code for those parts of the input code that belong to
-   --  the SPARK 2014 subset of Ada. Set True by the gnat2why executable or by
-   --  use of the -gnatd.F debug switch. Note that this is completely separate
-   --  from the SPARK restriction defined in GNAT to detect violations of a
-   --  subset of SPARK 2005 rules.
+   --  Specific compiling mode targeting formal verification for those parts
+   --  of the input code that belong to the SPARK 2014 subset of Ada. Set True
+   --  by the gnat2why executable or by use of the -gnatd.F debug switch. Note
+   --  that this is completely separate from the SPARK restriction defined in
+   --  GNAT to detect violations of a subset of SPARK 2005 rules.
 
    SPARK_Strict_Mode : Boolean := False;
    --  Interpret compiler permissions as strictly as possible. E.g. base ranges
diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb
index 6e1c250..4ad72df 100644
--- a/gcc/ada/sem_ch6.adb
+++ b/gcc/ada/sem_ch6.adb
@@ -10513,6 +10513,16 @@ package body Sem_Ch6 is
             if Scope (E) /= Current_Scope then
                null;
 
+            --  A function can overload the name of an abstract state. The
+            --  state can be viewed as a function with a profile that cannot
+            --  be matched by anything.
+
+            elsif Ekind (S) = E_Function
+              and then Ekind (E) = E_Abstract_State
+            then
+               Enter_Overloaded_Entity (S);
+               return;
+
             --  Ada 2012 (AI05-0165): For internally generated bodies of null
             --  procedures locate the internally generated spec. We enforce
             --  mode conformance since a tagged type may inherit from
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 7ab8c19..29240bc 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -284,6 +284,11 @@ package body Sem_Prag is
    --  determines if we have a body reference to an abstract state, which may
    --  be illegal if the state is refined within the body.
 
+   procedure Resolve_State (N : Node_Id);
+   --  Handle the overloading of state names by functions. When N denotes a
+   --  function, this routine finds the corresponding state and sets the entity
+   --  of N to that of the state.
+
    procedure Rewrite_Assertion_Kind (N : Node_Id);
    --  If N is Pre'Class, Post'Class, Invariant'Class, or Type_Invariant'Class,
    --  then it is rewritten as an identifier with the corresponding special
@@ -771,7 +776,8 @@ package body Sem_Prag is
                   Error_Msg_N ("cannot mix null and non-null items", Item);
                end if;
 
-               Analyze (Item);
+               Analyze       (Item);
+               Resolve_State (Item);
 
                --  Find the entity of the item. If this is a renaming, climb
                --  the renaming chain to reach the root object. Renamings of
@@ -1075,12 +1081,14 @@ package body Sem_Prag is
             if Nkind (Item) = N_Defining_Identifier then
                Item_Id := Item;
             else
-               Item_Id := Entity (Item);
+               Item_Id := Entity_Of (Item);
             end if;
 
             --  The item does not appear in a dependency
 
-            if not Contains (Used_Items, Item_Id) then
+            if Present (Item_Id)
+              and then not Contains (Used_Items, Item_Id)
+            then
                if Is_Formal (Item_Id) then
                   Usage_Error (Item, Item_Id);
 
@@ -1645,7 +1653,8 @@ package body Sem_Prag is
                return;
             end if;
 
-            Analyze (Item);
+            Analyze       (Item);
+            Resolve_State (Item);
 
             --  Find the entity of the item. If this is a renaming, climb the
             --  renaming chain to reach the root object. Renamings of non-
@@ -2262,10 +2271,11 @@ package body Sem_Prag is
                  ("cannot mix null and non-null initialization items", Item);
             end if;
 
-            Analyze (Item);
+            Analyze       (Item);
+            Resolve_State (Item);
 
             if Is_Entity_Name (Item) then
-               Item_Id := Entity (Item);
+               Item_Id := Entity_Of (Item);
 
                if Ekind_In (Item_Id, E_Abstract_State, E_Variable) then
 
@@ -2356,10 +2366,11 @@ package body Sem_Prag is
                     ("cannot mix null and non-null initialization item", Item);
                end if;
 
-               Analyze (Input);
+               Analyze       (Input);
+               Resolve_State (Input);
 
                if Is_Entity_Name (Input) then
-                  Input_Id := Entity (Input);
+                  Input_Id := Entity_Of (Input);
 
                   if Ekind_In (Input_Id, E_Abstract_State, E_Variable) then
 
@@ -21574,13 +21585,14 @@ package body Sem_Prag is
                     ("cannot mix null and non-null constituents", Constit);
                end if;
 
-               Analyze (Constit);
+               Analyze       (Constit);
+               Resolve_State (Constit);
 
                --  Ensure that the constituent denotes a valid state or a
                --  whole variable.
 
                if Is_Entity_Name (Constit) then
-                  Constit_Id := Entity (Constit);
+                  Constit_Id := Entity_Of (Constit);
 
                   if Ekind_In (Constit_Id, E_Abstract_State, E_Variable) then
                      Check_Matching_Constituent (Constit_Id);
@@ -21665,13 +21677,14 @@ package body Sem_Prag is
                  ("refinement clause cannot cover multiple states", State);
 
             else
-               Analyze (State);
+               Analyze       (State);
+               Resolve_State (State);
 
                --  Ensure that the state name denotes a valid abstract state
                --  that is defined in the spec of the related package.
 
                if Is_Entity_Name (State) then
-                  State_Id := Entity (State);
+                  State_Id := Entity_Of (State);
 
                   --  Catch any attempts to re-refine a state or refine a
                   --  state that is not defined in the package declaration.
@@ -21974,7 +21987,7 @@ package body Sem_Prag is
             if Nkind (Node (Elmt)) = N_Defining_Identifier then
                Id := Node (Elmt);
             else
-               Id := Entity (Node (Elmt));
+               Id := Entity_Of (Node (Elmt));
             end if;
 
             if Id = Item_Id then
@@ -23491,6 +23504,47 @@ package body Sem_Prag is
       end loop;
    end Relocate_Pragmas_To_Body;
 
+   -------------------
+   -- Resolve_State --
+   -------------------
+
+   procedure Resolve_State (N : Node_Id) is
+      Func  : Entity_Id;
+      State : Entity_Id;
+
+   begin
+      if Is_Entity_Name (N) and then Present (Entity (N)) then
+         Func := Entity (N);
+
+         --  Handle overloading of state names by functions. Traverse the
+         --  homonym chain looking for an abstract state.
+
+         if Ekind (Func) = E_Function and then Has_Homonym (Func) then
+            State := Homonym (Func);
+            while Present (State) loop
+
+               --  Resolve the overloading by setting the proper entity of the
+               --  reference to that of the state.
+
+               if Ekind (State) = E_Abstract_State then
+                  Set_Etype           (N, Standard_Void_Type);
+                  Set_Entity          (N, State);
+                  Set_Associated_Node (N, State);
+                  return;
+               end if;
+
+               State := Homonym (State);
+            end loop;
+
+            --  A function can never act as a state. If the homonym chain does
+            --  not contain a corresponding state, then something went wrong in
+            --  the overloading mechanism.
+
+            raise Program_Error;
+         end if;
+      end if;
+   end Resolve_State;
+
    ----------------------------
    -- Rewrite_Assertion_Kind --
    ----------------------------
diff --git a/gcc/ada/spark_xrefs.ads b/gcc/ada/spark_xrefs.ads
index 2b0a708..e7df033 100644
--- a/gcc/ada/spark_xrefs.ads
+++ b/gcc/ada/spark_xrefs.ads
@@ -56,8 +56,7 @@ package SPARK_Xrefs is
 
    --  SPARK cross-reference information is generated on a unit-by-unit basis
    --  in the ALI file, using lines that start with the identifying character F
-   --  ("Formal").  These lines are generated if -gnatd.E or -gnatd.F (Why
-   --  generation mode) switches are set.
+   --  ("Formal"). These lines are generated if Frame_Condition_Mode is True.
 
    --  The SPARK cross-reference information comes after the shared
    --  cross-reference information, so it needs not be read by tools like