[multiple changes]

2014-02-19  Yannick Moy  <moy@adacore.com>

	* sem_ch10.adb (Analyze_Proper_Body): Issue error on missing
	subunit in GNATprove_Mode.
	* sinfo.ads (GNATprove_Mode): Document error issued in GNATprove_Mode.

2014-02-19  Hristian Kirtchev  <kirtchev@adacore.com>

	* lib-xref.ads Alphabetize the contents of table
	Xref_Entity_Letters. Add an entry in table Xref_Entity_Letters
	for E_Abstract_State. List all letters and symbols in use.
	* sem_prag.adb (Analyze_Abstract_State): Update all calls
	to Create_Abstract_State to reflect the new signature.
	(Create_Abstract_State): Change subprogram profile and update
	the comment on usage. Use the proper location of the state
	declaration when creating a new abstract state entity. Do not
	generate an external name, but simply reuse the name coming from
	the state declaration.

From-SVN: r207884

5 files changed, 128 insertions, 110 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 1892dbf..588729f 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,22 @@
+2014-02-19  Yannick Moy  <moy@adacore.com>
+
+	* sem_ch10.adb (Analyze_Proper_Body): Issue error on missing
+	subunit in GNATprove_Mode.
+	* sinfo.ads (GNATprove_Mode): Document error issued in GNATprove_Mode.
+
+2014-02-19  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* lib-xref.ads Alphabetize the contents of table
+	Xref_Entity_Letters. Add an entry in table Xref_Entity_Letters
+	for E_Abstract_State. List all letters and symbols in use.
+	* sem_prag.adb (Analyze_Abstract_State): Update all calls
+	to Create_Abstract_State to reflect the new signature.
+	(Create_Abstract_State): Change subprogram profile and update
+	the comment on usage. Use the proper location of the state
+	declaration when creating a new abstract state entity. Do not
+	generate an external name, but simply reuse the name coming from
+	the state declaration.
+
 2014-02-19  Robert Dewar  <dewar@adacore.com>
 
 	* exp_ch4.adb (Expand_N_Expression_With_Actions): Make sure
diff --git a/gcc/ada/lib-xref.ads b/gcc/ada/lib-xref.ads
index b8f3e55..3f1a301 100644
--- a/gcc/ada/lib-xref.ads
+++ b/gcc/ada/lib-xref.ads
@@ -433,95 +433,87 @@ package Lib.Xref is
    --  indicating procedures and functions. If the operation is abstract,
    --  these letters are replaced in the xref by 'x' and 'y' respectively.
 
-   Xref_Entity_Letters : array (Entity_Kind) of Character :=
-     (E_Void                                       => ' ',
-      E_Variable                                   => '*',
-      E_Component                                  => '*',
-      E_Constant                                   => '*',
-      E_Discriminant                               => '*',
-
-      E_Loop_Parameter                             => '*',
-      E_In_Parameter                               => '*',
-      E_Out_Parameter                              => '*',
-      E_In_Out_Parameter                           => '*',
-      E_Generic_In_Out_Parameter                   => '*',
-
-      E_Generic_In_Parameter                       => '*',
-      E_Named_Integer                              => 'N',
-      E_Named_Real                                 => 'N',
-      E_Enumeration_Type                           => 'E',  -- B for boolean
-      E_Enumeration_Subtype                        => 'E',  -- B for boolean
+   --  The following letters and symbols are currently in use:
+   --    A B C D E F I K L M N O P   R S T U V W X Y
+   --    a b c d e f i k l m n o p q r s t u v w x y
+   --    @ * + space
 
-      E_Signed_Integer_Type                        => 'I',
-      E_Signed_Integer_Subtype                     => 'I',
-      E_Modular_Integer_Type                       => 'M',
-      E_Modular_Integer_Subtype                    => 'M',
-      E_Ordinary_Fixed_Point_Type                  => 'O',
-
-      E_Ordinary_Fixed_Point_Subtype               => 'O',
-      E_Decimal_Fixed_Point_Type                   => 'D',
-      E_Decimal_Fixed_Point_Subtype                => 'D',
-      E_Floating_Point_Type                        => 'F',
-      E_Floating_Point_Subtype                     => 'F',
-
-      E_Access_Type                                => 'P',
-      E_Access_Subtype                             => 'P',
+   Xref_Entity_Letters : array (Entity_Kind) of Character :=
+     (E_Abstract_State                             => '@',
       E_Access_Attribute_Type                      => 'P',
-      E_Allocator_Type                             => ' ',
-      E_General_Access_Type                        => 'P',
-
-      E_Access_Subprogram_Type                     => 'P',
       E_Access_Protected_Subprogram_Type           => 'P',
-      E_Anonymous_Access_Subprogram_Type           => ' ',
+      E_Access_Subprogram_Type                     => 'P',
+      E_Access_Subtype                             => 'P',
+      E_Access_Type                                => 'P',
+      E_Allocator_Type                             => ' ',
       E_Anonymous_Access_Protected_Subprogram_Type => ' ',
+      E_Anonymous_Access_Subprogram_Type           => ' ',
       E_Anonymous_Access_Type                      => ' ',
-
-      E_Array_Type                                 => 'A',
       E_Array_Subtype                              => 'A',
-      E_String_Type                                => 'S',
-      E_String_Subtype                             => 'S',
-      E_String_Literal_Subtype                     => ' ',
-
-      E_Class_Wide_Type                            => 'C',
+      E_Array_Type                                 => 'A',
+      E_Block                                      => 'q',
       E_Class_Wide_Subtype                         => 'C',
-      E_Record_Type                                => 'R',
-      E_Record_Subtype                             => 'R',
-      E_Record_Type_With_Private                   => 'R',
-
-      E_Record_Subtype_With_Private                => 'R',
-      E_Private_Type                               => '+',
-      E_Private_Subtype                            => '+',
-      E_Limited_Private_Type                       => '+',
-      E_Limited_Private_Subtype                    => '+',
-
-      E_Incomplete_Type                            => '+',
-      E_Incomplete_Subtype                         => '+',
-      E_Task_Type                                  => 'T',
-      E_Task_Subtype                               => 'T',
-      E_Protected_Type                             => 'W',
-
-      E_Protected_Subtype                          => 'W',
-      E_Exception_Type                             => ' ',
-      E_Subprogram_Type                            => ' ',
-      E_Enumeration_Literal                        => 'n',
-      E_Function                                   => 'V',
-
-      E_Operator                                   => 'V',
-      E_Procedure                                  => 'U',
+      E_Class_Wide_Type                            => 'C',
+      E_Component                                  => '*',
+      E_Constant                                   => '*',
+      E_Decimal_Fixed_Point_Subtype                => 'D',
+      E_Decimal_Fixed_Point_Type                   => 'D',
+      E_Discriminant                               => '*',
       E_Entry                                      => 'Y',
       E_Entry_Family                               => 'Y',
-      E_Block                                      => 'q',
-
       E_Entry_Index_Parameter                      => '*',
+      E_Enumeration_Literal                        => 'n',
+      E_Enumeration_Subtype                        => 'E',  -- B for boolean
+      E_Enumeration_Type                           => 'E',  -- B for boolean
       E_Exception                                  => 'X',
+      E_Exception_Type                             => ' ',
+      E_Floating_Point_Subtype                     => 'F',
+      E_Floating_Point_Type                        => 'F',
+      E_Function                                   => 'V',
+      E_General_Access_Type                        => 'P',
       E_Generic_Function                           => 'v',
+      E_Generic_In_Out_Parameter                   => '*',
+      E_Generic_In_Parameter                       => '*',
       E_Generic_Package                            => 'k',
       E_Generic_Procedure                          => 'u',
-
       E_Label                                      => 'L',
+      E_Limited_Private_Subtype                    => '+',
+      E_Limited_Private_Type                       => '+',
       E_Loop                                       => 'l',
-      E_Return_Statement                           => ' ',
+      E_Loop_Parameter                             => '*',
+      E_In_Out_Parameter                           => '*',
+      E_In_Parameter                               => '*',
+      E_Incomplete_Subtype                         => '+',
+      E_Incomplete_Type                            => '+',
+      E_Modular_Integer_Subtype                    => 'M',
+      E_Modular_Integer_Type                       => 'M',
+      E_Named_Integer                              => 'N',
+      E_Named_Real                                 => 'N',
+      E_Operator                                   => 'V',
+      E_Ordinary_Fixed_Point_Subtype               => 'O',
+      E_Ordinary_Fixed_Point_Type                  => 'O',
+      E_Out_Parameter                              => '*',
       E_Package                                    => 'K',
+      E_Private_Subtype                            => '+',
+      E_Private_Type                               => '+',
+      E_Procedure                                  => 'U',
+      E_Protected_Subtype                          => 'W',
+      E_Protected_Type                             => 'W',
+      E_Record_Subtype                             => 'R',
+      E_Record_Subtype_With_Private                => 'R',
+      E_Record_Type                                => 'R',
+      E_Record_Type_With_Private                   => 'R',
+      E_Return_Statement                           => ' ',
+      E_Signed_Integer_Subtype                     => 'I',
+      E_Signed_Integer_Type                        => 'I',
+      E_String_Literal_Subtype                     => ' ',
+      E_String_Subtype                             => 'S',
+      E_String_Type                                => 'S',
+      E_Subprogram_Type                            => ' ',
+      E_Task_Subtype                               => 'T',
+      E_Task_Type                                  => 'T',
+      E_Variable                                   => '*',
+      E_Void                                       => ' ',
 
       --  The following entities are not ones to which we gather the cross-
       --  references, since it does not make sense to do so (e.g. references to
@@ -529,15 +521,10 @@ package Lib.Xref is
       --  body entity is considered to be a reference to the spec entity.
 
       E_Package_Body                               => ' ',
-      E_Protected_Object                           => ' ',
       E_Protected_Body                             => ' ',
-      E_Task_Body                                  => ' ',
+      E_Protected_Object                           => ' ',
       E_Subprogram_Body                            => ' ',
-
-      --  ??? The following letter is added for completion, proper design and
-      --  implementation of abstract state cross-referencing to follow.
-
-      E_Abstract_State                             => ' ');
+      E_Task_Body                                  => ' ');
 
    --  The following table is for information purposes. It shows the use of
    --  each character appearing as an entity type.
diff --git a/gcc/ada/sem_ch10.adb b/gcc/ada/sem_ch10.adb
index b72fdd3..1b35930 100644
--- a/gcc/ada/sem_ch10.adb
+++ b/gcc/ada/sem_ch10.adb
@@ -1563,8 +1563,9 @@ package body Sem_Ch10 is
       procedure Optional_Subunit;
       --  This procedure is called when the main unit is a stub, or when we
       --  are not generating code. In such a case, we analyze the subunit if
-      --  present, which is user-friendly and in fact required for ASIS, but
-      --  we don't complain if the subunit is missing.
+      --  present, which is user-friendly and in fact required for ASIS, but we
+      --  don't complain if the subunit is missing. In GNATprove_Mode, we issue
+      --  an error to avoid formal verification of a partial unit.
 
       ----------------------
       -- Optional_Subunit --
@@ -1579,18 +1580,18 @@ package body Sem_Ch10 is
          --  ignore all errors. Note that Fatal_Error will still be set, so we
          --  will be able to check for this case below.
 
-         if not ASIS_Mode then
+         if not (ASIS_Mode or GNATprove_Mode) then
             Ignore_Errors_Enable := Ignore_Errors_Enable + 1;
          end if;
 
          Unum :=
            Load_Unit
              (Load_Name  => Subunit_Name,
-              Required   => False,
+              Required   => GNATprove_Mode,
               Subunit    => True,
               Error_Node => N);
 
-         if not ASIS_Mode then
+         if not (ASIS_Mode or GNATprove_Mode) then
             Ignore_Errors_Enable := Ignore_Errors_Enable - 1;
          end if;
 
diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb
index 42c7076..5357230 100644
--- a/gcc/ada/sem_prag.adb
+++ b/gcc/ada/sem_prag.adb
@@ -9986,14 +9986,16 @@ package body Sem_Prag is
                --  Opt is not a duplicate property and sets the flag Status.
 
                procedure Create_Abstract_State
-                 (State_Nam  : Name_Id;
-                  State_Decl : Node_Id;
-                  Is_Null    : Boolean := False);
-               --  Generate an abstract state entity with name State_Nam and
-               --  enter it into visibility. State_Decl is the "declaration"
-               --  of the state as it appears in pragma Abstract_State. Flag
-               --  Is_Null should be set when the associated Abstract_State
-               --  pragma defines a null state.
+                 (Nam     : Name_Id;
+                  Decl    : Node_Id;
+                  Loc     : Source_Ptr;
+                  Is_Null : Boolean);
+               --  Generate an abstract state entity with name Nam and enter it
+               --  into visibility. Decl is the "declaration" of the state as
+               --  it appears in pragma Abstract_State. Loc is the location of
+               --  the related state "declaration". Flag Is_Null should be set
+               --  when the associated Abstract_State pragma defines a null
+               --  state.
 
                -----------------------------
                -- Analyze_External_Option --
@@ -10243,17 +10245,16 @@ package body Sem_Prag is
                ---------------------------
 
                procedure Create_Abstract_State
-                 (State_Nam  : Name_Id;
-                  State_Decl : Node_Id;
-                  Is_Null    : Boolean := False)
+                 (Nam     : Name_Id;
+                  Decl    : Node_Id;
+                  Loc     : Source_Ptr;
+                  Is_Null : Boolean)
                is
                begin
                   --  The generated state abstraction reuses the same chars
                   --  from the original state declaration. Decorate the entity.
 
-                  State_Id :=
-                    Make_Defining_Identifier (Sloc (State),
-                      Chars => New_External_Name (State_Nam));
+                  State_Id := Make_Defining_Identifier (Loc, Nam);
 
                   --  Null states never come from source
 
@@ -10270,15 +10271,16 @@ package body Sem_Prag is
                   --  N_Null and does not carry any linkages.
 
                   if not Is_Null then
-                     if Present (State_Decl) then
-                        Set_Entity (State_Decl, State_Id);
-                        Set_Etype  (State_Decl, Standard_Void_Type);
+                     if Present (Decl) then
+                        Set_Entity (Decl, State_Id);
+                        Set_Etype  (Decl, Standard_Void_Type);
                      end if;
 
-                     --  Every non-null state must be nameable and resolvable
-                     --  the same way a constant is.
+                     --  Every non-null state must be defined, nameable and
+                     --  resolvable.
 
                      Push_Scope (Pack_Id);
+                     Generate_Definition (State_Id);
                      Enter_Name (State_Id);
                      Pop_Scope;
                   end if;
@@ -10303,9 +10305,10 @@ package body Sem_Prag is
 
                elsif Nkind (State) = N_Null then
                   Create_Abstract_State
-                    (State_Nam  => New_Internal_Name ('S'),
-                     State_Decl => Empty,
-                     Is_Null    => True);
+                    (Nam     => New_Internal_Name ('S'),
+                     Decl    => Empty,
+                     Loc     => Sloc (State),
+                     Is_Null => True);
                   Null_Seen := True;
 
                   --  Catch a case where a null state appears in a list of
@@ -10321,8 +10324,10 @@ package body Sem_Prag is
 
                elsif Nkind (State) = N_Identifier then
                   Create_Abstract_State
-                    (State_Nam  => Chars (State),
-                     State_Decl => State);
+                    (Nam     => Chars (State),
+                     Decl    => State,
+                     Loc     => Sloc (State),
+                     Is_Null => False);
                   Non_Null_Seen := True;
 
                --  State declaration with various options. This construct
@@ -10331,8 +10336,10 @@ package body Sem_Prag is
                elsif Nkind (State) = N_Extension_Aggregate then
                   if Nkind (Ancestor_Part (State)) = N_Identifier then
                      Create_Abstract_State
-                       (State_Nam  => Chars (Ancestor_Part (State)),
-                        State_Decl => Ancestor_Part (State));
+                       (Nam     => Chars (Ancestor_Part (State)),
+                        Decl    => Ancestor_Part (State),
+                        Loc     => Sloc (Ancestor_Part (State)),
+                        Is_Null => False);
                      Non_Null_Seen := True;
                   else
                      Error_Msg_N
diff --git a/gcc/ada/sinfo.ads b/gcc/ada/sinfo.ads
index ee35965..b5769f8 100644
--- a/gcc/ada/sinfo.ads
+++ b/gcc/ada/sinfo.ads
@@ -552,6 +552,10 @@ package Sinfo is
    --  In addition pragma Debug statements are removed from the tree (rewritten
    --  to NULL stmt), since they should be taken into account in flow analysis.
 
+   --  An error is also issued for missing subunits, similar to the warning
+   --  issued when generating code, to avoid formal verification of a partial
+   --  unit.
+
    -----------------------
    -- Check Flag Fields --
    -----------------------