* Code reorganization for GNATProve GPL2014

examples/aadlv2/producer_consumer/producer_consumer.adb

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---                 Copyright (C) 2009, GET-Telecom Paris.                   --
+--       Copyright (C) 2009 Telecom ParisTech, 2010-2014 ESA & ISAE.        --
 --                                                                          --
 -- PolyORB HI is free software; you  can  redistribute  it and/or modify it --
 -- under terms of the GNU General Public License as published by the Free   --
@@ -26,7 +26,8 @@
 -- however invalidate  any other reasons why  the executable file  might be --
 -- covered by the  GNU Public License.                                      --
 --                                                                          --
---                PolyORB HI is maintained by GET Telecom Paris             --
+--              PolyORB-HI/Ada is maintained by the TASTE project           --
+--                      (taste-users@lists.tuxfamily.org)                   --
 --                                                                          --
 ------------------------------------------------------------------------------
 
@@ -61,6 +62,11 @@ package body Producer_Consumer is
    procedure Produce_Spg (Data_Source : out Alpha_Type) is
    begin
       Data_Source := The_Data;
+
+      if The_Data > 1000 then
+         The_Data := 1;
+      end if;
+
       The_Data := The_Data + 1;
 
       Put_Line (Normal, Get_Node

src/Makefile.am

@@ -16,6 +16,7 @@ ADA_SPECS_WITH_BODY = $(srcdir)/polyorb_hi-aperiodic_task.ads	\
 	 $(srcdir)/polyorb_hi-suspenders.ads			\
 	 $(srcdir)/polyorb_hi-thread_interrogators.ads		\
 	 $(srcdir)/polyorb_hi-scheduler.ads			\
+	 $(srcdir)/polyorb_hi-time_marshallers.ads		\
 	 $(srcdir)/polyorb_hi-unprotected_queue.ads		\
 	 $(srcdir)/polyorb_hi-utils.ads
 
@@ -25,7 +26,6 @@ ADA_SPECS = $(ADA_SPECS_WITH_BODY) $(srcdir)/polyorb_hi.ads	\
 	$(srcdir)/polyorb_hi-output_low_level.ads		\
 	$(srcdir)/polyorb_hi-port_type_marshallers.ads		\
 	$(srcdir)/polyorb_hi-streams.ads			\
-	$(srcdir)/polyorb_hi-time_marshallers.ads		\
 	$(srcdir)/polyorb_hi-transport_low_level.ads
 
 ADA_BODIES = $(ADA_SPECS_WITH_BODY:.ads=.adb)			\

src/native.adc

 --  Ada restrictions to be supported by PolyORB HI, for native targets
- 
---  pragma Profile_Warnings (Ravenscar);              -- D.13.1
- 
+
+pragma Profile_Warnings (Ravenscar);              -- D.13.1

src/polyorb_hi-messages.ads

@@ -118,8 +118,9 @@ private
    end record;
 
    function Valid (Message : Message_Type) return Boolean is
-      (Message.First >= Message.Content'First and then Message.First < Message.Last
-      and then Message.Last <= Message.Content'Last);
+      (Message.First >= Message.Content'First
+         and then Message.First < Message.Last
+         and then Message.Last <= Message.Content'Last);
 
    function Payload (M : Message_Type) return Stream_Element_Array is
       (M.Content (M.First .. M.Last));

src/polyorb_hi-null_task.adb

@@ -31,19 +31,14 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
-with Ada.Synchronous_Task_Control;
-
 with PolyORB_HI.Output;
-with PolyORB_HI.Suspenders;
 
 package body PolyORB_HI.Null_Task is
 
    use PolyORB_HI.Errors;
    use PolyORB_HI.Output;
    use PolyORB_HI_Generated.Deployment;
-   use PolyORB_HI.Suspenders;
    use Ada.Real_Time;
-   use Ada.Synchronous_Task_Control;
 
    -------------------
    -- The_Null_Task --
@@ -51,11 +46,15 @@ package body PolyORB_HI.Null_Task is
 
    procedure The_Null_Task is
       Error : Error_Kind;
+      Initialized : Boolean := True;
 
    begin
       --  Run the initialize entrypoint (if any)
 
-      Activate_Entrypoint;
+      if not Initialized then
+         Activate_Entrypoint;
+         Initialized := True;
+      end if;
 
       --  Wait for the network initialization to be finished
 

src/polyorb_hi-null_task.ads

@@ -31,6 +31,13 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
+--  Define a "null" task as a job to be scheduled by a
+--  software-defined scheduler in place of a OS scheduler. Its
+--  interface mimics the one of a periodic task.
+--
+--  Expected usage is for a Round-Robin non-preemptive scheduler
+--  defined through a cyclic function.
+
 with System;
 with Ada.Real_Time;
 with PolyORB_HI_Generated.Deployment;
@@ -65,6 +72,13 @@ generic
    --  detected.
 
 package PolyORB_HI.Null_Task is
+   --  The following parameters are not used for now. The usage is
+   --  reserved for future extensions.
+
+   pragma Unreferenced (Task_Priority);
+   pragma Unreferenced (Task_Stack_Size);
+   pragma Unreferenced (Task_Period);
+   pragma Unreferenced (Task_Deadline);
 
    procedure The_Null_Task;
 

src/polyorb_hi-thread_interrogators.adb

@@ -59,7 +59,6 @@ package body PolyORB_HI.Thread_Interrogators is
       Integer_Array,
       Port_Kind_Array,
       Port_Image_Array,
-      Address_Array,
       Overflow_Protocol_Array,
       Thread_Interface_Type,
       Current_Entity,
@@ -70,238 +69,50 @@ package body PolyORB_HI.Thread_Interrogators is
       Thread_Fifo_Offsets,
       Thread_Overflow_Protocols,
       Urgencies,
-      Global_Data_Queue_Size,
-      N_Destinations,
-      Destinations,
-      Marshall,
-      Next_Deadline);
+      Global_Data_Queue_Size);
    use UQ;
 
-   ------------------
-   -- Global_Queue --
-   ------------------
-
-   --  The protected object below handles all the received events or
-   --  data on IN ports.
-   --
-   --  Finally, the protected object contains a second array to store
-   --  the number of received values for each IN EVENT [DATA] (0 .. n)
-   --  and IN DATA (0 .. 1) port.
-
-   protected Global_Queue is
-      pragma Priority (System.Priority'Last);
-
-      entry Wait_Event (P : out Port_Type);
-      --  Blocks until the thread receives a new event. Return the
-      --  corresponding Port that received the event.
-
-      procedure Read_Event (P : out Port_Type; Valid : out Boolean);
-      --  Same as 'Wait_Event' but without blocking. Valid is set to
-      --  False if there is nothing to receive.
-
-      procedure Dequeue (T : Port_Type; P : out Port_Stream_Entry);
-      --  Dequeue a value from the partial FIFO of port T. If there is
-      --  no enqueued value, return the latest dequeued value.
-
-      function Read_In (T : Port_Type) return Port_Stream_Entry;
-      --  Read the oldest queued value on the partial FIFO of IN port
-      --  T without dequeuing it. If there is no queued value, return
-      --  the latest dequeued value.
-
-      function Read_Out (T : Port_Type) return Port_Stream_Entry;
-      --  Return the value put for OUT port T.
-
-      function Is_Invalid (T : Port_Type) return Boolean;
-      --  Return True if no Put_Value has been called for this port
-      --  since the last Set_Invalid call.
-
-      procedure Set_Invalid (T : Port_Type);
-      --  Set the value stored for OUT port T as invalid to impede its
-      --  future sending without calling Put_Value. This procedure is
-      --  generally called just after Read_Out. However we cannot
-      --  combine them in one routine because we need Read_Out to be a
-      --  function and functions cannot modify protected object
-      --  states.
-
-      procedure Store_In (P : Port_Stream_Entry; T : Time);
-      --  Stores a new incoming message in its corresponding
-      --  position. If this is an event [data] incoming message, then
-      --  stores it in the queue, updates its most recent value and
-      --  unblock the barrier. Otherwise, it only overrides the most
-      --  recent value. T is the time stamp associated to the port
-      --  P. In case of data ports with delayed connections, it
-      --  indicates the instant from which the data of P becomes
-      --  deliverable.
-
-      procedure Store_Out (P : Port_Stream_Entry; T : Time);
-      --  Store a value of an OUT port to be sent at the next call to
-      --  Send_Output and mark the value as valid.
-
-      function Count (T : Port_Type) return Integer;
-      --  Return the number of pending messages on IN port T.
-
-      function Get_Time_Stamp (P : Port_Type) return Time;
-      --  Return the time stamp associated to port T
-
-   private
-
-      Not_Empty : Boolean := False;
-      --  The protected object barrier. True when there is at least
-      --  one pending event [data].
-
-   end Global_Queue;
-
-   protected body Global_Queue is
-
-      ----------------
-      -- Wait_Event --
-      ----------------
-
-      entry Wait_Event (P : out Port_Type) when Not_Empty is
-         Valid : Boolean;
-      begin
-         UQ.Read_Event (P, Valid, Not_Empty);
-
-         pragma Debug (Put_Line
-                       (Verbose,
-                        CE
-                        + ": Wait_Event: oldest unread event port = "
-                        + Thread_Port_Images (P)));
-      end Wait_Event;
-
-      ----------------
-      -- Read_Event --
-      ----------------
-
-      procedure Read_Event (P : out Port_Type; Valid : out Boolean) is
-      begin
-         UQ.Read_Event (P, Valid, Not_Empty);
-      end Read_Event;
-
-      -------------
-      -- Dequeue --
-      -------------
-
-      procedure Dequeue (T : Port_Type; P : out Port_Stream_Entry) is
-      begin
-         UQ.Dequeue (T, P, Not_Empty);
-      end Dequeue;
-
-      -------------
-      -- Read_In --
-      -------------
-
-      function Read_In (T : Port_Type) return Port_Stream_Entry is
-      begin
-         return UQ.Read_In (T);
-      end Read_In;
-
-      --------------
-      -- Read_Out --
-      --------------
-
-      function Read_Out (T : Port_Type) return Port_Stream_Entry is
-      begin
-         return UQ.Read_Out (T);
-      end Read_Out;
-
-      ----------------
-      -- Is_Invalid --
-      ----------------
-
-      function Is_Invalid (T : Port_Type) return Boolean is
-      begin
-         return UQ.Is_Invalid (T);
-      end Is_Invalid;
-
-      -----------------
-      -- Set_Invalid --
-      -----------------
-
-      procedure Set_Invalid (T : Port_Type) is
-      begin
-         UQ.Set_Invalid (T);
-      end Set_Invalid;
-
-      --------------
-      -- Store_In --
-      --------------
-
-      procedure Store_In (P : Port_Stream_Entry; T : Time) is
-      begin
-         UQ.Store_In (P, T, Not_Empty);
-      end Store_In;
-
-      ---------------
-      -- Store_Out --
-      ---------------
-
-      procedure Store_Out (P : Port_Stream_Entry; T : Time) is
-      begin
-         UQ.Store_Out (P, T);
-      end Store_Out;
-
-      -----------
-      -- Count --
-      -----------
-
-      function Count (T : Port_Type) return Integer is
-      begin
-         return UQ.Count (T);
-      end Count;
-
-      --------------------
-      -- Get_Time_Stamp --
-      --------------------
-
-      function Get_Time_Stamp (P : Port_Type) return Time is
-      begin
-         return UQ.Get_Time_Stamp (P);
-      end Get_Time_Stamp;
-
-   end Global_Queue;
-
    -----------------
    -- Send_Output --
    -----------------
 
    function Send_Output (Port : Port_Type) return Error_Kind is
 
-      type Port_Type_Array is array (Positive)
-        of PolyORB_HI_Generated.Deployment.Port_Type;
-      type Port_Type_Array_Access is access Port_Type_Array;
+       type Port_Type_Array is array (Positive)
+         of PolyORB_HI_Generated.Deployment.Port_Type;
+        type Port_Type_Array_Access is access Port_Type_Array;
 
-      function To_Pointer is new Ada.Unchecked_Conversion
-        (System.Address, Port_Type_Array_Access);
+        function To_Pointer is new Ada.Unchecked_Conversion
+          (System.Address, Port_Type_Array_Access);
 
-      Dst       : constant Port_Type_Array_Access :=
-        To_Pointer (Destinations (Port));
-      N_Dst     : Integer renames N_Destinations (Port);
-      P_Kind    : Port_Kind renames Thread_Port_Kinds (Port);
+        Dst       : constant Port_Type_Array_Access :=
+          To_Pointer (Destinations (Port));
+        N_Dst     : Integer renames N_Destinations (Port);
+        P_Kind    : Port_Kind renames Thread_Port_Kinds (Port);
 
-      Message   : aliased PolyORB_HI.Messages.Message_Type;
-      Value     : constant Thread_Interface_Type := Stream_To_Interface
-        (Global_Queue.Read_Out (Port).Payload);
+        Message   : PolyORB_HI.Messages.Message_Type;
+        Value     : constant Thread_Interface_Type := Stream_To_Interface
+          (UQ.Read_Out (Port).Payload);
 
       Error : Error_Kind := Error_None;
    begin
       pragma Debug (Put_Line (Verbose,
                               CE
-                              + ": Send_Output: port "
-                              + Thread_Port_Images (Port)));
+                                + ": Send_Output: port "
+                                + Thread_Port_Images (Port)));
 
       --  If no valid value is to be sent, quit
 
-      if Global_Queue.Is_Invalid (Port) then
+      if UQ.Is_Invalid (Port) then
          pragma Debug (Put_Line (Verbose,
                                  CE
-                                 + ": Send_Output: Invalid value in port "
-                                 + Thread_Port_Images (Port)));
+                                   + ": Send_Output: Invalid value in port "
+                                   + Thread_Port_Images (Port)));
          null;
       else
          --  Mark the port value as invalid to impede future sendings
 
-         Global_Queue.Set_Invalid (Port);
+         UQ.Set_Invalid (Port);
 
          --  Begin the sending to all destinations
 
@@ -315,7 +126,7 @@ package body PolyORB_HI.Thread_Interrogators is
 
             if not Is_Event (P_Kind) then
                Time_Marshallers.Marshall
-                 (Global_Queue.Get_Time_Stamp (Port),
+                 (UQ.Get_Time_Stamp (Port),
                   Message);
             end if;
 
@@ -327,10 +138,10 @@ package body PolyORB_HI.Thread_Interrogators is
               (Put_Line
                (Verbose,
                 CE
-                + ": Send_Output: to port "
-                + PolyORB_HI_Generated.Deployment.Port_Image (Dst (To))
-                + " of "
-                + Entity_Image (Port_Table (Dst (To)))));
+                  + ": Send_Output: to port "
+                  + PolyORB_HI_Generated.Deployment.Port_Image (Dst (To))
+                  + " of "
+                  + Entity_Image (Port_Table (Dst (To)))));
 
             Error := Protocols.Send (Current_Entity,
                                      Port_Table (Dst (To)),
@@ -345,9 +156,9 @@ package body PolyORB_HI.Thread_Interrogators is
 
          pragma Debug (Put_Line (Verbose,
                                  CE
-                                 + ": Send_Output: port "
-                                 + Thread_Port_Images (Port)
-                                 + ". End."));
+                                   + ": Send_Output: port "
+                                   + Thread_Port_Images (Port)
+                                   + ". End."));
       end if;
 
       return Error;
@@ -361,7 +172,7 @@ package body PolyORB_HI.Thread_Interrogators is
    begin
       pragma Debug (Put_Line (Verbose, CE + ": Put_Value"));
 
-      Global_Queue.Store_Out
+      UQ.Store_Out
         ((Current_Entity, Interface_To_Stream (Thread_Interface)),
          Next_Deadline);
    end Put_Value;
@@ -373,7 +184,7 @@ package body PolyORB_HI.Thread_Interrogators is
    procedure Receive_Input (Port : Port_Type) is
       pragma Unreferenced (Port);
    begin
-      raise Program_Error with CE + ": Receive_Input: Not implemented yet";
+      null; -- XXX Cannot raise an exception here
    end Receive_Input;
 
    ---------------
@@ -381,7 +192,7 @@ package body PolyORB_HI.Thread_Interrogators is
    ---------------
 
    function Get_Value (Port : Port_Type) return Thread_Interface_Type is
-      Stream : constant Port_Stream := Global_Queue.Read_In (Port).Payload;
+      Stream : constant Port_Stream := UQ.Read_In (Port).Payload;
       T_Port : constant Thread_Interface_Type := Stream_To_Interface (Stream);
    begin
       pragma Debug (Put_Line
@@ -398,7 +209,7 @@ package body PolyORB_HI.Thread_Interrogators is
    ----------------
 
    function Get_Sender (Port : Port_Type) return Entity_Type is
-      Sender : constant Entity_Type := Global_Queue.Read_In (Port).From;
+      Sender : constant Entity_Type := UQ.Read_In (Port).From;
    begin
       pragma Debug (Put_Line
                     (Verbose,
@@ -415,7 +226,7 @@ package body PolyORB_HI.Thread_Interrogators is
    ---------------
 
    function Get_Count (Port : Port_Type) return Integer is
-      Count : constant Integer := Global_Queue.Count (Port);
+      Count : constant Integer := UQ.Count (Port);
    begin
       pragma Debug (Put_Line (Verbose,
                               CE
@@ -433,13 +244,14 @@ package body PolyORB_HI.Thread_Interrogators is
 
    procedure Next_Value (Port : Port_Type) is
       P : Port_Stream_Entry;
+      Not_Empty : Boolean;
    begin
       pragma Debug (Put_Line (Verbose,
                               CE
                               + ": Next_Value for port "
                               + Thread_Port_Images (Port)));
 
-      Global_Queue.Dequeue (Port, P);
+      UQ.Dequeue (Port, P, Not_Empty);
    end Next_Value;
 
    ------------------------------
@@ -447,10 +259,14 @@ package body PolyORB_HI.Thread_Interrogators is
    ------------------------------
 
    procedure Wait_For_Incoming_Events (Port : out Port_Type) is
+      Valid, Not_Empty : Boolean;
+      pragma Warnings (Off, Not_Empty);
+      --  Under this implementation, Not_Empty is not used.
+
    begin
       pragma Debug (Put_Line (Verbose, CE + ": Wait_For_Incoming_Events"));
 
-      Global_Queue.Wait_Event (Port);
+      UQ.Read_Event (Port, Valid, Not_Empty);
 
       pragma Debug (Put_Line
                     (Verbose,
@@ -465,8 +281,11 @@ package body PolyORB_HI.Thread_Interrogators is
    --------------------