This patch corrects the mechanism which handles limited with clauses to semi-
declare abstract states (the states are fully declared when Abstract_States is
analyzed). The end result is that multiple limited with clauses now reference
one unique entity which denotes the state.
------------
-- Source --
------------
-- aip.ads
package AIP with SPARK_Mode is
pragma Pure;
end AIP;
-- aip-ip.ads
limited with AIP.UDP;
limited with AIP.TCP;
package AIP.IP with
SPARK_Mode,
Abstract_State => (FIB, State),
Initializes => (FIB, State)
is
procedure IP_Input (Netif : Integer; Buf : Integer) with
Global => (Input => (FIB, UDP.State),
In_Out => (TCP.State, State));
pragma Export (C, IP_Input, "AIP_ip_input");
end AIP.IP;
-- aip-ip.adb
with AIP.UDP;
with AIP.TCP;
package body AIP.IP with
SPARK_Mode,
Refined_State => (State => IP_Serial,
FIB => Default_Router)
is
Default_Router : Integer := 0;
IP_Serial : Integer := 0;
procedure IP_Input (Netif : Integer; Buf : Integer) with
Refined_Global => (Input => (Default_Router, UDP.State),
In_Out => (IP_Serial, TCP.State))
is
begin
null;
end IP_Input;
end AIP.IP;
-- aip-tcp.ads
limited with AIP.IP;
package AIP.TCP with
SPARK_Mode,
Abstract_State => State
is
procedure TCP_Input (Buf : Integer; Netif : Integer) with
Global => (Input => IP.FIB,
In_Out => (IP.State, State));
end AIP.TCP;
-- aip-udp.ads
with AIP.IP;
package AIP.UDP with
SPARK_Mode,
Abstract_State => State
is
procedure UDP_Input (Buf : Integer; Netif : Integer) with
Global => (Input => State);
end AIP.UDP;
-----------------
-- Compilation --
-----------------
$ gcc -c aip-ip.adb
Tested on x86_64-pc-linux-gnu, committed on trunk
2014-07-31 Hristian Kirtchev <[email protected]>
* sem_ch10.adb (Process_State): Remove local variable Name. Add
local variable Decl. Partially declare an abstract state by
generating an entity and storing it in the state declaration.
* sem_prag.adb (Create_Abstract_State): Fully declare a
semi-declared abstract state.
Index: sem_ch10.adb
===================================================================
--- sem_ch10.adb (revision 213264)
+++ sem_ch10.adb (working copy)
@@ -5695,10 +5695,10 @@
procedure Process_State (State : Node_Id) is
Loc : constant Source_Ptr := Sloc (State);
+ Decl : Node_Id;
+ Dummy : Entity_Id;
Elmt : Node_Id;
Id : Entity_Id;
- Name : Name_Id;
- Dummy : Entity_Id;
begin
-- Multiple abstract states appear as an aggregate
@@ -5721,12 +5721,12 @@
-- extension aggregate.
elsif Nkind (State) = N_Extension_Aggregate then
- Name := Chars (Ancestor_Part (State));
+ Decl := Ancestor_Part (State);
-- Simple state declaration
elsif Nkind (State) = N_Identifier then
- Name := Chars (State);
+ Decl := State;
-- Possibly an illegal state declaration
@@ -5734,15 +5734,27 @@
return;
end if;
- -- Construct a dummy state for the purposes of establishing a
- -- non-limited => limited view relation. Note that the dummy
- -- state is not added to list Abstract_States to avoid multiple
- -- definitions.
+ -- Abstract states are elaborated when the related pragma is
+ -- elaborated. Since the withed package is not analyzed yet,
+ -- the entities of the abstract states are not available. To
+ -- overcome this complication, create the entities now and
+ -- store them in their respective declarations. The entities
+ -- are later used by routine Create_Abstract_State to declare
+ -- and enter the states into visibility.
- Id := Make_Defining_Identifier (Loc, New_External_Name (Name));
- Set_Parent (Id, State);
- Decorate_State (Id, Scop);
+ if No (Entity (Decl)) then
+ Id := Make_Defining_Identifier (Loc, Chars (Decl));
+ Set_Entity (Decl, Id);
+ Set_Parent (Id, State);
+ Decorate_State (Id, Scop);
+
+ -- Otherwise the package was previously withed
+
+ else
+ Id := Entity (Decl);
+ end if;
+
Build_Shadow_Entity (Id, Scop, Dummy);
end Process_State;
Index: sem_prag.adb
===================================================================
--- sem_prag.adb (revision 213271)
+++ sem_prag.adb (working copy)
@@ -10519,11 +10519,24 @@
Is_Null : Boolean)
is
begin
- -- The generated state abstraction reuses the same chars
- -- from the original state declaration. Decorate the entity.
+ -- The abstract state may be semi-declared when the related
+ -- package was withed through a limited with clause. In that
+ -- case reuse the entity to fully declare the state.
- State_Id := Make_Defining_Identifier (Loc, Nam);
+ if Present (Decl) and then Present (Entity (Decl)) then
+ State_Id := Entity (Decl);
+ -- Otherwise the elaboration of pragma Abstract_State
+ -- declares the state.
+
+ else
+ State_Id := Make_Defining_Identifier (Loc, Nam);
+
+ if Present (Decl) then
+ Set_Entity (Decl, State_Id);
+ end if;
+ end if;
+
-- Null states never come from source
Set_Comes_From_Source (State_Id, not Is_Null);
