[Ada] Missing error on illegal initialization item

Message ID 20171215132504.GA17856@adacore.com
State New
Headers show
Series
  • [Ada] Missing error on illegal initialization item
Related show

Commit Message

Pierre-Marie de Rodat Dec. 15, 2017, 1:25 p.m.
This patch modifies the analysis of pragma Initializes to detect an illegal
null initialization item.

------------
-- Source --
------------

--  remote.ads

package Remote is
   Y : Integer := 0;
end Remote;

--  pack.ads

with Remote;

package Pack
   with SPARK_Mode,
        Initializes => (null => Remote.Y)
is
   X : Integer := 0;
end Pack;

----------------------------
-- Compilation and output --
----------------------------

$ gcc -c pack.ads
pack.ads:5:25: initialization item must denote object or state

Tested on x86_64-pc-linux-gnu, committed on trunk

2017-12-15  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_prag.adb (Analyze_Initialization_Item): Remove the specialized
	processing for a null initialization item. Such an item is always
	illegal.

Patch

Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 255692)
+++ sem_prag.adb	(working copy)
@@ -2752,10 +2752,6 @@ 
       --  A list of all initialization items processed so far. This list is
       --  used to detect duplicate items.
 
-      Non_Null_Seen : Boolean := False;
-      Null_Seen     : Boolean := False;
-      --  Flags used to check the legality of a null initialization list
-
       States_And_Objs : Elist_Id := No_Elist;
       --  A list of all abstract states and objects declared in the visible
       --  declarations of the related package. This list is used to detect the
@@ -2785,91 +2781,67 @@ 
          Item_Id : Entity_Id;
 
       begin
-         --  Null initialization list
+         Analyze       (Item);
+         Resolve_State (Item);
 
-         if Nkind (Item) = N_Null then
-            if Null_Seen then
-               SPARK_Msg_N ("multiple null initializations not allowed", Item);
+         if Is_Entity_Name (Item) then
+            Item_Id := Entity_Of (Item);
 
-            elsif Non_Null_Seen then
-               SPARK_Msg_N
-                 ("cannot mix null and non-null initialization items", Item);
-            else
-               Null_Seen := True;
-            end if;
+            if Present (Item_Id)
+              and then Ekind_In (Item_Id, E_Abstract_State,
+                                          E_Constant,
+                                          E_Variable)
+            then
+               --  When the initialization item is undefined, it appears as
+               --  Any_Id. Do not continue with the analysis of the item.
 
-         --  Initialization item
+               if Item_Id = Any_Id then
+                  null;
 
-         else
-            Non_Null_Seen := True;
+               --  The state or variable must be declared in the visible
+               --  declarations of the package (SPARK RM 7.1.5(7)).
 
-            if Null_Seen then
-               SPARK_Msg_N
-                 ("cannot mix null and non-null initialization items", Item);
-            end if;
+               elsif not Contains (States_And_Objs, Item_Id) then
+                  Error_Msg_Name_1 := Chars (Pack_Id);
+                  SPARK_Msg_NE
+                    ("initialization item & must appear in the visible "
+                     & "declarations of package %", Item, Item_Id);
 
-            Analyze       (Item);
-            Resolve_State (Item);
+               --  Detect a duplicate use of the same initialization item
+               --  (SPARK RM 7.1.5(5)).
 
-            if Is_Entity_Name (Item) then
-               Item_Id := Entity_Of (Item);
+               elsif Contains (Items_Seen, Item_Id) then
+                  SPARK_Msg_N ("duplicate initialization item", Item);
 
-               if Present (Item_Id)
-                 and then Ekind_In (Item_Id, E_Abstract_State,
-                                             E_Constant,
-                                             E_Variable)
-               then
-                  --  When the initialization item is undefined, it appears as
-                  --  Any_Id. Do not continue with the analysis of the item.
+               --  The item is legal, add it to the list of processed states
+               --  and variables.
 
-                  if Item_Id = Any_Id then
-                     null;
+               else
+                  Append_New_Elmt (Item_Id, Items_Seen);
 
-                  --  The state or variable must be declared in the visible
-                  --  declarations of the package (SPARK RM 7.1.5(7)).
-
-                  elsif not Contains (States_And_Objs, Item_Id) then
-                     Error_Msg_Name_1 := Chars (Pack_Id);
-                     SPARK_Msg_NE
-                       ("initialization item & must appear in the visible "
-                        & "declarations of package %", Item, Item_Id);
-
-                  --  Detect a duplicate use of the same initialization item
-                  --  (SPARK RM 7.1.5(5)).
-
-                  elsif Contains (Items_Seen, Item_Id) then
-                     SPARK_Msg_N ("duplicate initialization item", Item);
-
-                  --  The item is legal, add it to the list of processed states
-                  --  and variables.
-
-                  else
-                     Append_New_Elmt (Item_Id, Items_Seen);
-
-                     if Ekind (Item_Id) = E_Abstract_State then
-                        Append_New_Elmt (Item_Id, States_Seen);
-                     end if;
-
-                     if Present (Encapsulating_State (Item_Id)) then
-                        Append_New_Elmt (Item_Id, Constits_Seen);
-                     end if;
+                  if Ekind (Item_Id) = E_Abstract_State then
+                     Append_New_Elmt (Item_Id, States_Seen);
                   end if;
 
-               --  The item references something that is not a state or object
-               --  (SPARK RM 7.1.5(3)).
-
-               else
-                  SPARK_Msg_N
-                    ("initialization item must denote object or state", Item);
+                  if Present (Encapsulating_State (Item_Id)) then
+                     Append_New_Elmt (Item_Id, Constits_Seen);
+                  end if;
                end if;
 
-            --  Some form of illegal construct masquerading as a name
-            --  (SPARK RM 7.1.5(3)). This is a syntax error, always report.
+            --  The item references something that is not a state or object
+            --  (SPARK RM 7.1.5(3)).
 
             else
-               Error_Msg_N
+               SPARK_Msg_N
                  ("initialization item must denote object or state", Item);
             end if;
+
+         --  Some form of illegal construct masquerading as a name
+         --  (SPARK RM 7.1.5(3)). This is a syntax error, always report.
+
+         else
+            Error_Msg_N
+              ("initialization item must denote object or state", Item);
          end if;
       end Analyze_Initialization_Item;