This is the mail archive of the gcc-patches@gcc.gnu.org mailing list for the GCC project.


Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]
Other format: [Raw text]

[Ada] Interplay between limited with clauses, abstract states and refinement


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  <kirtchev@adacore.com>

	* 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.

Attachment: difs
Description: Text document


Index Nav: [Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav: [Date Prev] [Date Next] [Thread Prev] [Thread Next]