Ensure that session state is not changed by user-defined function

[treiher]

The private part of the session context contains the current state of the state machine and the state of the memory allocator. The context is a tagged type.

   type Private_Context is private;

   type Context is abstract tagged limited
      record
         P : Private_Context;
      end record;

private

   type Private_Context is
      record
         Next_State : State := S_Start;
         Slots : Test.Session_Allocator.Slots;
         Memory : Test.Session_Allocator.Memory;
      end record;

User-defined functions are realized as abstract primitives. It must be ensured that a user-defined function does not modify the private part of a session context. Unfortunately, using the Old attribute is not possible in that case:

   procedure Foo (Ctx : in out Context; Bar : RFLX.Test.Baz; RFLX_Result : out Boolean) is abstract with
     Post'Class =>
       Ctx.P = Ctx.P'Old;

rflx-test-session.ads:30:08: error: equality on access types is not allowed in SPARK
   30 |       Ctx.P = Ctx.P'Old;
      |       ^~~~~~~~~~~~~~~~~
  violation of aspect SPARK_Mode at line 16
   16 |  SPARK_Mode
      |  ^ here

rflx-test-session.ads:30:16: error: prefix of "Old" attribute which is not a function call is not allowed in SPARK (SPARK RM 3.10(13))
   30 |       Ctx.P = Ctx.P'Old;
      |               ^~~~~
  violation of aspect SPARK_Mode at line 16
   16 |  SPARK_Mode
      |  ^ here

[jklmnn]

One problem with this behavior is that it prevents the proof of the remaining unit. To work around this maybe a ghost variable with an assume can be used in the following way:

   Ghost_Context : Private_Context with Ghost;
begin
   Ghost_Context := Ctx.P;
   Foo (Ctx, Result);
   pragma Assume (Ctx.P = Ghost_Context);

One problem is that we might run into the same problem as above that equality on access types is not allowed in SPARK.

[jklmnn]

After an offline discussion we came to the conclusion that we cannot prove that the private part of a context is unchanged after a platform function call. This change could happen by calling Tick on the context in the platform function. The correct way to go here is to check all required properties after each platform function call.