===================================================================
@@ -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;
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.