sem_prag.adb (Analyze_Pragma): Remove the detection of a useless Part_Of indicator when...

2015-05-22  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_prag.adb (Analyze_Pragma): Remove the detection
	of a useless Part_Of indicator when the related item is a constant.
	(Check_Matching_Constituent): Do not emit an error on a constant.
	(Check_Missing_Part_Of): Do not check for a missing Part_Of indicator
	when the related item is a constant.
	(Collect_Body_States): Code cleanup.
	(Collect_Visible_States): Code cleanup.
	(Report_Unused_States): Do not emit an error on a constant.
	* sem_util.ads, sem_util.adb (Has_Variable_Input): Removed.

From-SVN: r223535

gcc/ada/ChangeLog

+2015-05-22  Hristian Kirtchev  <kirtchev@adacore.com>
+
+	* sem_prag.adb (Analyze_Pragma): Remove the detection
+	of a useless Part_Of indicator when the related item is a constant.
+	(Check_Matching_Constituent): Do not emit an error on a constant.
+	(Check_Missing_Part_Of): Do not check for a missing Part_Of indicator
+	when the related item is a constant.
+	(Collect_Body_States): Code cleanup.
+	(Collect_Visible_States): Code cleanup.
+	(Report_Unused_States): Do not emit an error on a constant.
+	* sem_util.ads, sem_util.adb (Has_Variable_Input): Removed.
+
 2015-05-22  Eric Botcazou  <ebotcazou@adacore.com>
 
 	* sem_ch8.adb (Analyze_Object_Renaming): Copy

gcc/ada/sem_prag.adb

@@ -17555,20 +17555,6 @@ package body Sem_Prag is
                Legal   => Legal);
 
             if Legal then
-
-               --  Constants without "variable input" are not considered part
-               --  of the hidden state of a package (SPARK RM 7.1.1(2)). As a
-               --  result such constants do not require a Part_Of indicator.
-
-               if Ekind (Item_Id) = E_Constant
-                 and then not Has_Variable_Input (Item_Id)
-               then
-                  SPARK_Msg_NE
-                    ("useless Part_Of indicator, constant & does not have "
-                     & "variable input", N, Item_Id);
-                  return;
-               end if;
-
                State_Id := Entity (State);
 
                --  The Part_Of indicator turns an object into a constituent of
@@ -23983,14 +23969,25 @@ package body Sem_Prag is
                      end loop;
                   end if;
 
+                  --  Constants are part of the hidden state of a package, but
+                  --  the compiler cannot determine whether they have variable
+                  --  input (SPARK RM 7.1.1(2)) and cannot classify them as a
+                  --  hidden state. Accept the constant quietly even if it is
+                  --  a visible state or lacks a Part_Of indicator.
+
+                  if Ekind (Constit_Id) = E_Constant then
+                     null;
+
                   --  If we get here, then the constituent is not a hidden
                   --  state of the related package and may not be used in a
                   --  refinement (SPARK RM 7.2.2(9)).
 
-                  Error_Msg_Name_1 := Chars (Spec_Id);
-                  SPARK_Msg_NE
-                    ("cannot use & in refinement, constituent is not a hidden "
-                     & "state of package %", Constit, Constit_Id);
+                  else
+                     Error_Msg_Name_1 := Chars (Spec_Id);
+                     SPARK_Msg_NE
+                       ("cannot use & in refinement, constituent is not a "
+                        & "hidden state of package %", Constit, Constit_Id);
+                  end if;
                end if;
             end Check_Matching_Constituent;
 
@@ -24434,7 +24431,6 @@ package body Sem_Prag is
          ----------------------------
 
          procedure Collect_Visible_States (Pack_Id : Entity_Id) is
-            Decl    : Node_Id;
             Item_Id : Entity_Id;
 
          begin
@@ -24453,27 +24449,15 @@ package body Sem_Prag is
                elsif Ekind (Item_Id) = E_Abstract_State then
                   Add_Item (Item_Id, Result);
 
-               elsif Ekind_In (Item_Id, E_Constant, E_Variable) then
-                  Decl := Declaration_Node (Item_Id);
-
-                  --  Do not consider constants or variables that map generic
-                  --  formals to their actuals as the formals cannot be named
-                  --  from the outside and participate in refinement.
-
-                  if Present (Corresponding_Generic_Association (Decl)) then
-                     null;
-
-                  --  Constants without "variable input" are not considered a
-                  --  hidden state of a package (SPARK RM 7.1.1(2)).
-
-                  elsif Ekind (Item_Id) = E_Constant
-                    and then not Has_Variable_Input (Item_Id)
-                  then
-                     null;
+               --  Do not consider constants or variables that map generic
+               --  formals to their actuals, as the formals cannot be named
+               --  from the outside and participate in refinement.
 
-                  else
-                     Add_Item (Item_Id, Result);
-                  end if;
+               elsif Ekind_In (Item_Id, E_Constant, E_Variable)
+                 and then No (Corresponding_Generic_Association
+                                (Declaration_Node (Item_Id)))
+               then
+                  Add_Item (Item_Id, Result);
 
                --  Recursively gather the visible states of a nested package
 
@@ -24562,31 +24546,39 @@ package body Sem_Prag is
             while Present (State_Elmt) loop
                State_Id := Node (State_Elmt);
 
+               --  Constants are part of the hidden state of a package, but the
+               --  compiler cannot determine whether they have variable input
+               --  (SPARK RM 7.1.1(2)) and cannot classify them properly as a
+               --  hidden state. Do not emit an error when a constant does not
+               --  participate in a state refinement, even though it acts as a
+               --  hidden state.
+
+               if Ekind (State_Id) = E_Constant then
+                  null;
+
                --  Generate an error message of the form:
 
                --    body of package ... has unused hidden states
                --      abstract state ... defined at ...
-               --      constant ... defined at ...
                --      variable ... defined at ...
 
-               if not Posted then
-                  Posted := True;
-                  SPARK_Msg_N
-                    ("body of package & has unused hidden states", Body_Id);
-               end if;
-
-               Error_Msg_Sloc := Sloc (State_Id);
+               else
+                  if not Posted then
+                     Posted := True;
+                     SPARK_Msg_N
+                       ("body of package & has unused hidden states", Body_Id);
+                  end if;
 
-               if Ekind (State_Id) = E_Abstract_State then
-                  SPARK_Msg_NE
-                    ("\abstract state & defined #", Body_Id, State_Id);
+                  Error_Msg_Sloc := Sloc (State_Id);
 
-               elsif Ekind (State_Id) = E_Constant then
-                  SPARK_Msg_NE ("\constant & defined #", Body_Id, State_Id);
+                  if Ekind (State_Id) = E_Abstract_State then
+                     SPARK_Msg_NE
+                       ("\abstract state & defined #", Body_Id, State_Id);
 
-               else
-                  pragma Assert (Ekind (State_Id) = E_Variable);
-                  SPARK_Msg_NE ("\variable & defined #", Body_Id, State_Id);
+                  else
+                     pragma Assert (Ekind (State_Id) = E_Variable);
+                     SPARK_Msg_NE ("\variable & defined #", Body_Id, State_Id);
+                  end if;
                end if;
 
                Next_Elmt (State_Elmt);
@@ -25017,12 +25009,11 @@ package body Sem_Prag is
       elsif SPARK_Mode /= On then
          return;
 
-      --  Do not consider constants without variable input because those are
-      --  not part of the hidden state of a package (SPARK RM 7.1.1(2)).
+      --  Do not consider constants, because the compiler cannot accurately
+      --  determine whether they have variable input (SPARK RM 7.1.1(2)) and
+      --  act as a hidden state of a package.
 
-      elsif Ekind (Item_Id) = E_Constant
-        and then not Has_Variable_Input (Item_Id)
-      then
+      elsif Ekind (Item_Id) = E_Constant then
          return;
       end if;
 

gcc/ada/sem_util.adb

@@ -9317,17 +9317,6 @@ package body Sem_Util is
       end if;
    end Has_Tagged_Component;
 
-   ------------------------
-   -- Has_Variable_Input --
-   ------------------------
-
-   function Has_Variable_Input (Const_Id : Entity_Id) return Boolean is
-      Expr : constant Node_Id := Expression (Declaration_Node (Const_Id));
-   begin
-      return
-        Present (Expr) and then not Compile_Time_Known_Value_Or_Aggr (Expr);
-   end Has_Variable_Input;
-
    ----------------------------
    -- Has_Volatile_Component --
    ----------------------------

gcc/ada/sem_util.ads

@@ -1046,14 +1046,6 @@ package Sem_Util is
    --  component is present. This function is used to check if "=" has to be
    --  expanded into a bunch component comparisons.
 
-   function Has_Variable_Input (Const_Id : Entity_Id) return Boolean;
-   --  Determine whether the initialization expression of constant Const_Id has
-   --  "variable input" (SPARK RM 7.1.1(2)). This roughly maps to the semantic
-   --  concept of a compile-time known value.
-   --  How can a defined concept in SPARK mapped to an undefined predicate in
-   --  the compiler (which can change at any moment if the compiler feels like
-   --  getting more clever about what is compile-time known) ???
-
    function Has_Volatile_Component (Typ : Entity_Id) return Boolean;
    --  Given an arbitrary type, determine whether it contains at least one
    --  volatile component.