Fix proofs for GNAT CE 2020

ref #178

Author: jklmnn

src/memory/client/linux/gneiss-memory-client.adb

@@ -58,7 +58,10 @@ is
    end Initialize;
 
    procedure Modify (Session : in out Client_Session;
-                     Ctx     : in out Context)
+                     Ctx     : in out Context) with
+      SPARK_Mode => Off
+      --  Object_Size cannot be annotated to Buffer
+      --  This causes a check in the Address overlay
    is
       Length : constant Integer      := Gneiss_Internal.Syscall.Stat_Size (Session.Fd);
       Last   : constant Buffer_Index := Get_Last (Length);

src/memory/server/linux/gneiss-memory-server.adb

@@ -10,7 +10,10 @@ is
    function Get_Last is new Gneiss_Internal.Util.Get_Last (Buffer_Index);
 
    procedure Modify (Session : in out Server_Session;
-                     Ctx     : in out Context)
+                     Ctx     : in out Context) with
+      SPARK_Mode => Off
+      --  Object_Size cannot be annotated to Buffer
+      --  This causes a check in the Address overlay
    is
       Length : constant Integer      := Gneiss_Internal.Syscall.Stat_Size (Session.Fd);
       Last   : constant Buffer_Index := Get_Last (Length);

src/rom/client/linux/gneiss-rom-client.adb

@@ -40,7 +40,10 @@ is
    end Initialize;
 
    procedure Update (Session : in out Client_Session;
-                     Ctx     : in out Context)
+                     Ctx     : in out Context) with
+      SPARK_Mode => Off
+      --  Object_Size cannot be annotated to Buffer
+      --  This causes a check in the Address overlay
    is
       Length : constant Integer      := Gneiss_Internal.Syscall.Stat_Size (Session.Fd);
       Last   : constant Buffer_Index := Get_Last (Length);

test/hello_world/component.ads

@@ -6,7 +6,7 @@ with Gneiss_Internal;
 package Component with
    SPARK_Mode,
    Abstract_State => (Component_State, Platform_State),
-   Initializes => (Platform_State)
+   Initializes => (Platform_State, Main.Platform)
 is
 
    procedure Construct (Capability : Gneiss.Capability) with

test/linux.sh

@@ -10,14 +10,18 @@ make -C ada-runtime
 
 set -e
 
-./cement prove test/message_client.gpr . lib test -u component
-./cement prove test/message_server.gpr . lib test -u component
-./cement prove test/hello_world.gpr . lib test -u component
-./cement prove test/log_proxy.gpr . lib test -u component
-./cement prove test/rom.gpr . lib test -u component
-./cement prove test/memory_client.gpr . lib test -u component
-./cement prove test/memory_server.gpr . lib test -u component
-./cement prove test/timer.gpr . lib test -u component
+if [ "$(gcc -dumpversion)" = "9.3.1" ]
+then
+    # Only prove with GNAT CE 2020/GNAT Pro 21
+    ./cement prove test/message_client.gpr . lib test -u component
+    ./cement prove test/message_server.gpr . lib test -u component
+    ./cement prove test/hello_world.gpr . lib test -u component
+    ./cement prove test/log_proxy.gpr . lib test -u component
+    ./cement prove test/rom.gpr . lib test -u component
+    ./cement prove test/memory_client.gpr . lib test -u component
+    ./cement prove test/memory_server.gpr . lib test -u component
+    ./cement prove test/timer.gpr . lib test -u component
+fi
 
 ./cement build test/message_client/message_client.xml . lib test
 ./cement build test/hello_world/hello_world.xml . lib test

test/log_proxy/component.ads

@@ -6,7 +6,7 @@ with Gneiss_Internal;
 package Component with
    SPARK_Mode,
    Abstract_State => (Component_State, Platform_State),
-   Initializes    => (Platform_State)
+   Initializes    => (Platform_State, Main.Platform)
 is
 
    procedure Construct (Cap : Gneiss.Capability) with

test/memory_client/component.ads

@@ -6,7 +6,7 @@ with Gneiss.Component;
 package Component with
    SPARK_Mode,
    Abstract_State => Platform_State,
-   Initializes    => (Platform_State)
+   Initializes    => (Platform_State, Main.Platform)
 is
 
    procedure Construct (Cap : Gneiss.Capability) with

test/memory_server/component.ads

@@ -6,7 +6,7 @@ with Gneiss_Internal;
 package Component with
 SPARK_Mode,
    Abstract_State => (Component_State, Platform_State),
-   Initializes    => (Platform_State)
+   Initializes    => (Platform_State, Main.Platform)
 is
 
    procedure Construct (Cap : Gneiss.Capability) with

test/message_client/component.ads

@@ -6,7 +6,7 @@ with Gneiss_Internal;
 package Component with
    SPARK_Mode,
    Abstract_State => (Component_State, Platform_State),
-   Initializes    => (Platform_State)
+   Initializes    => (Platform_State, Main.Platform)
 is
 
    procedure Construct (Cap : Gneiss.Capability) with

test/message_server/component.ads

@@ -6,7 +6,7 @@ with Gneiss_Internal;
 package Component with
    SPARK_Mode,
    Abstract_State => (Component_State, Platform_State),
-   Initializes    => (Platform_State)
+   Initializes    => (Platform_State, Main.Platform)
 is
 
    procedure Construct (Cap : Gneiss.Capability) with

test/rom/component.ads

@@ -6,7 +6,7 @@ with Gneiss_Internal;
 package Component with
    SPARK_Mode,
    Abstract_State => (Component_State, Platform_State),
-   Initializes    => (Platform_State)
+   Initializes    => (Platform_State, Main.Platform)
 is
 
    procedure Construct (Capability : Gneiss.Capability) with

test/timer/component.ads

@@ -6,7 +6,7 @@ with Gneiss_Internal;
 package Component with
    SPARK_Mode,
    Abstract_State => (Component_State, Platform_State),
-   Initializes    => (Platform_State)
+   Initializes    => (Platform_State, Main.Platform)
 is
 
    procedure Construct (Cap : Gneiss.Capability) with