improve contracts of block client and server

ref #80
Componolit · Aug 8, 2019 · dca8713 · dca8713
1 parent 011813a
commit dca8713
Show file tree

Hide file tree

Showing 4 changed files with 30 additions and 14 deletions.
diff --git a/src/block/client/componolit-interfaces-block-client.ads b/src/block/client/componolit-interfaces-block-client.ads
@@ -83,7 +83,8 @@ is
    --
    --  @param R  Request
    --  @return   Request status
-   function Status (R : Request) return Request_Status;
+   function Status (R : Request) return Request_Status with
+      Annotate => (GNATprove, Terminating);
 
    --  Get request start block
    --
@@ -127,9 +128,13 @@ is
                                L :        Count;
                                I :        Request_Id;
                                E :    out Result) with
-      Pre            => Initialized (C) and then Status (R) = Raw,
-      Contract_Cases => (E = Success => Status (R) = Allocated,
-                         others      => Status (R) = Raw);
+      Pre  => Initialized (C)
+              and Status (R) = Raw,
+      Post => Initialized (C)
+              and Writable (C)'Old    = Writable (C)
+              and Block_Count (C)'Old = Block_Count (C)
+              and Block_Size (C)'Old  = Block_Size (C)
+              and (if E = Success then Status (R) = Allocated else Status (R) = Raw);
 
    --  Checks if a request has been changed by the platform
    --
@@ -140,7 +145,10 @@ is
       Pre  => Initialized (C)
               and Status (R) = Pending,
       Post => Initialized (C)
-              and Status (R) in Pending | Ok | Error;
+              and Status (R) in Pending | Ok | Error
+              and Writable (C)'Old    = Writable (C)
+              and Block_Count (C)'Old = Block_Count (C)
+              and Block_Size (C)'Old  = Block_Size (C);
 
    --  Return True if C is initialized
    --

diff --git a/src/block/client/genode/componolit-interfaces-block-client.adb b/src/block/client/genode/componolit-interfaces-block-client.adb
@@ -112,21 +112,24 @@ is
       end if;
    end Allocate_Request;
 
+   procedure Update_Response_Queue (C : in out Client_Session;
+                                    H : in out Request_Handle);
+
    pragma Warnings (Off, "formal parameter ""C"" is not modified");
    --  Cxx.Block.Client.Update_Response_Queue modifies state
    procedure Update_Response_Queue (C : in out Client_Session;
                                     H : in out Request_Handle)
    is
-      State   : Integer;
-      Success : Integer;
-      Tag     : Cxx.Unsigned_Long;
+      State : Integer;
+      Succ  : Integer;
+      Tag   : Cxx.Unsigned_Long;
    begin
       if not H.Valid then
-         Cxx.Block.Client.Update_Response_Queue (C.Instance, State, Tag, Success);
+         Cxx.Block.Client.Update_Response_Queue (C.Instance, State, Tag, Succ);
          if State = 1 then
             H := Request_Handle'(Valid   => True,
                                  Tag     => Tag,
-                                 Success => Success = 1);
+                                 Success => Succ = 1);
          end if;
       end if;
    end Update_Response_Queue;

diff --git a/src/block/server/componolit-interfaces-block-dispatcher.ads b/src/block/server/componolit-interfaces-block-dispatcher.ads
@@ -49,7 +49,8 @@ is
    --  @param D    Dispatcher session instance
    --  @param Cap  System capability
    procedure Initialize (D   : in out Dispatcher_Session;
-                         Cap :        Componolit.Interfaces.Types.Capability);
+                         Cap :        Componolit.Interfaces.Types.Capability) with
+      Pre => not Initialized (D);
 
    --  Register the server implementation Serv on the platform
    --
@@ -87,7 +88,8 @@ is
       Pre  => Initialized (D)
               and then Valid_Session_Request (D, C)
               and then not Serv.Initialized (I),
-      Post => Initialized (D);
+      Post => Initialized (D)
+      and then Valid_Session_Request (D, C);
 
    --  Accept session request
    --
@@ -100,7 +102,8 @@ is
       Pre  => Initialized (D)
               and then Valid_Session_Request (D, C)
               and then Serv.Initialized (I),
-      Post => Initialized (D);
+      Post => Initialized (D)
+      and then not Valid_Session_Request (D, C);
 
    --  Garbage collects disconnected sessions
    --

diff --git a/src/block/server/componolit-interfaces-block-server.ads b/src/block/server/componolit-interfaces-block-server.ads
@@ -182,7 +182,9 @@ is
    --  If this procedure is not called at least once before returning from the event handler a deadlock might occur.
    --
    --  @param S  Server session instance
-   procedure Unblock_Client (S : in out Server_Session);
+   procedure Unblock_Client (S : in out Server_Session) with
+      Pre  => Initialized (S),
+      Post => Initialized (S);
 
 private