prove global state of timer client

ref #164
Componolit · Apr 24, 2020 · 0c92318 · 0c92318
1 parent f748543
commit 0c92318
Show file tree

Hide file tree

Showing 4 changed files with 40 additions and 15 deletions.
diff --git a/src/timer/client/gneiss-timer-client.ads b/src/timer/client/gneiss-timer-client.ads
@@ -8,6 +8,7 @@
 --  This file is part of Gneiss, which is distributed under the terms of the
 --  GNU Affero General Public License version 3.
 --
+with Gneiss_Internal;
 
 generic
    --  Timer event
@@ -23,7 +24,8 @@ is
    procedure Initialize (C     : in out Client_Session;
                          Cap   :        Capability;
                          Label :        String;
-                         Idx   :        Session_Index := 1);
+                         Idx   :        Session_Index := 1) with
+      Global => (In_Out => Gneiss_Internal.Platform_State);
 
    --  Returns a monotonic clock value
    --
@@ -34,7 +36,8 @@ is
    --  @return   Current clock value
    function Clock (C : Client_Session) return Time with
       Volatile_Function,
-      Pre => Initialized (C);
+      Pre    => Initialized (C),
+      Global => (Input => Gneiss_Internal.Platform_State);
 
    --  Sets the timeout after which the Event procedure will be called
    --
@@ -48,14 +51,16 @@ is
    --  @param D  Timeout event duration
    procedure Set_Timeout (C : in out Client_Session;
                           D :        Duration) with
-      Pre  => Initialized (C)
-              and then D > 0.0,
-      Post => Initialized (C);
+      Pre    => Initialized (C)
+                and then D > 0.0,
+      Post   => Initialized (C),
+      Global => (In_Out => Gneiss_Internal.Platform_State);
 
    --  Finalizes timer session
    --
    --  @param C  Timer client session object
    procedure Finalize (C : in out Client_Session) with
-      Post => not Initialized (C);
+      Post   => not Initialized (C),
+      Global => (In_Out => Gneiss_Internal.Platform_State);
 
 end Gneiss.Timer.Client;
diff --git a/src/timer/client/linux/gneiss-timer-client.adb b/src/timer/client/linux/gneiss-timer-client.adb
@@ -1,6 +1,5 @@
 
 with System;
-with Gneiss_Internal;
 with Gneiss_Internal.Epoll;
 with Gneiss_Internal.Syscall;
 with Gneiss_Internal.Client;
@@ -24,18 +23,21 @@ is
                         D  : Duration) with
       Import,
       Convention    => C,
-      External_Name => "gneiss_timer_set";
+      External_Name => "gneiss_timer_set",
+      Global        => (In_Out => Gneiss_Internal.Platform_State);
 
    function Timer_Get (Fd : Gneiss_Internal.File_Descriptor) return Time with
       Import,
       Convention    => C,
       External_Name => "gneiss_timer_get",
+      Global        => (Input => Gneiss_Internal.Platform_State),
       Volatile_Function;
 
    procedure Timer_Read (Fd : Gneiss_Internal.File_Descriptor) with
       Import,
       Convention    => C,
-      External_Name => "gneiss_timer_read";
+      External_Name => "gneiss_timer_read",
+      Global        => (In_Out => Gneiss_Internal.Platform_State);
 
    function Event_Address (Session : Client_Session) return System.Address with
       SPARK_Mode => Off
@@ -81,7 +83,9 @@ is
       C.Index := Session_Index_Option'(Valid => True, Value => Idx);
    end Initialize;
 
-   function Clock (C : Client_Session) return Time
+   function Clock (C : Client_Session) return Time with
+      SPARK_Mode => Off
+      --  Clock is not recognized as volatile even though Timer_Get is
    is
    begin
       return Timer_Get (C.Fd);

diff --git a/test/timer/component.adb b/test/timer/component.adb
@@ -6,9 +6,15 @@ with Gneiss.Timer.Client;
 with Basalt.Strings;
 
 package body Component with
-   SPARK_Mode
+   SPARK_Mode,
+   Refined_State => (Component_State => Capability,
+                     Platform_State  => (Log, Timer))
 is
-   procedure Event;
+   procedure Event with
+      Global => (In_Out => (Log,
+                            Gneiss_Internal.Platform_State,
+                            Main.Platform),
+                 Input  => (Capability, Timer));
 
    package Gneiss_Log is new Gneiss.Log;
    package Gneiss_Timer is new Gneiss.Timer;

diff --git a/test/timer/component.ads b/test/timer/component.ads
@@ -1,13 +1,23 @@
 
 with Gneiss;
 with Gneiss.Component;
+with Gneiss_Internal;
 
 package Component with
-   SPARK_Mode
+   SPARK_Mode,
+   Abstract_State => (Component_State, Platform_State),
+   Initializes    => (Main.Platform, Platform_State)
 is
 
-   procedure Construct (Cap : Gneiss.Capability);
-   procedure Destruct;
+   procedure Construct (Cap : Gneiss.Capability) with
+      Global => (Output => Component_State,
+                 In_Out => (Platform_State,
+                            Main.Platform,
+                            Gneiss_Internal.Platform_State));
+
+   procedure Destruct with
+      Global => (In_Out => (Platform_State,
+                            Gneiss_Internal.Platform_State));
 
    package Main is new Gneiss.Component (Construct, Destruct);