prove global state of memory client

ref #164
Componolit · May 20, 2020 · ee2bd2e · ee2bd2e
1 parent 4ebda50
commit ee2bd2e
Show file tree

Hide file tree

Showing 4 changed files with 30 additions and 17 deletions.
diff --git a/src/memory/client/gneiss-memory-client.ads b/src/memory/client/gneiss-memory-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
    pragma Warnings (Off, "* is not referenced");
@@ -34,7 +35,8 @@ is
                          Cap     :        Capability;
                          Label   :        String;
                          Size    :        Long_Integer;
-                         Idx     :        Session_Index := 1);
+                         Idx     :        Session_Index := 1) with
+      Global => (In_Out => Gneiss_Internal.Platform_State);
 
    --  Access the shared memory buffer, this will call the passed Modify procedure
    --
@@ -43,15 +45,17 @@ is
       with function Contract (Ctx : Context) return Boolean;
    procedure Modify (Session : in out Client_Session;
                      Ctx     : in out Context) with
-      Pre  => Initialized (Session)
-              and then Contract (Ctx),
-      Post => Initialized (Session)
-              and then Contract (Ctx);
+      Pre    => Initialized (Session)
+                and then Contract (Ctx),
+      Post   => Initialized (Session)
+                and then Contract (Ctx),
+      Global => (In_Out => Gneiss_Internal.Platform_State);
 
    --  Close session
    --
    --  @param Session  Client session
    procedure Finalize (Session : in out Client_Session) with
-      Post => not Initialized (Session);
+      Post   => not Initialized (Session),
+      Global => (In_Out => Gneiss_Internal.Platform_State);
 
 end Gneiss.Memory.Client;
diff --git a/src/memory/client/linux/gneiss-memory-client.adb b/src/memory/client/linux/gneiss-memory-client.adb
@@ -1,6 +1,5 @@
 
 with System;
-with Gneiss_Internal;
 with Gneiss_Internal.Syscall;
 with Gneiss_Internal.Client;
 with Gneiss_Protocol.Session;
@@ -14,7 +13,8 @@ is
                            Fd   : out Gneiss_Internal.File_Descriptor) with
       Import,
       Convention    => C,
-      External_Name => "gneiss_memfd_create";
+      External_Name => "gneiss_memfd_create",
+      Global        => (In_Out => Gneiss_Internal.Platform_State);
 
    function Get_First (Length : Integer) return Buffer_Index;
    function Get_Last (Length : Integer) return Buffer_Index;

diff --git a/test/memory_client/component.adb b/test/memory_client/component.adb
@@ -5,7 +5,8 @@ with Gneiss.Memory;
 with Gneiss.Memory.Client;
 
 package body Component with
-   SPARK_Mode
+   SPARK_Mode,
+   Refined_State => (Platform_State => (Log, Mem))
 is
 
    package Gneiss_Log is new Gneiss.Log;
@@ -18,11 +19,11 @@ is
    procedure Modify (Session : in out Memory.Client_Session;
                      Data    : in out String;
                      Ctx     : in out Gneiss_Log.Client_Session) with
-      Pre  => Memory.Initialized (Session)
-              and then Gneiss_Log.Initialized (Ctx),
-      Post => Memory.Initialized (Session)
-              and then Gneiss_Log.Initialized (Ctx),
-      Global => null;
+      Pre    => Memory.Initialized (Session)
+                and then Gneiss_Log.Initialized (Ctx),
+      Post   => Memory.Initialized (Session)
+                and then Gneiss_Log.Initialized (Ctx),
+      Global => (In_Out => Gneiss_Internal.Platform_State);
 
    package Memory_Client is new Memory.Client (Gneiss_Log.Client_Session, Modify);
 

diff --git a/test/memory_client/component.ads b/test/memory_client/component.ads
@@ -1,13 +1,21 @@
 
+with Gneiss_Internal;
 with Gneiss;
 with Gneiss.Component;
 
 package Component with
-   SPARK_Mode
+   SPARK_Mode,
+   Abstract_State => Platform_State,
+   Initializes    => (Platform_State, Main.Platform)
 is
 
-   procedure Construct (Cap : Gneiss.Capability);
-   procedure Destruct;
+   procedure Construct (Cap : Gneiss.Capability) with
+      Global => (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);