[Spark] How to terminate information flow?

[Lutz Donnerhacke <lutz@iks-jena.de>]

I came across a strange situation drop loss of information and do not know
how to annotate that.

[xxx.ads]
   --  NAME
   --         exit - terminate the current process
   --  SYNOPSIS
   --         void _exit(int status);
   procedure sysexit (return_code : exit_code_t);
   --# global in out Kernel.State;
   --# derives Kernel.State from Kernel.State, return_code;
   pragma Inline_Always (sysexit);

[xxx.adb]
   procedure sysexit (return_code : exit_code_t) is
      res : long;
      ok  : Boolean;
   begin
      syscall1(Linux_i86.sys_exit, long(return_code), res, ok);
   end sysexit;

[yyy.ads]
   procedure syscall1 (nr : syscall_number; a1 : long;
     res : out long; ok : out Boolean);
   --# global in out Kernel.State;
   --# derives Kernel.State from Kernel.State, nr, a1 &
   --#         res, ok      from Kernel.State, a1;
   --# post (not ok and -res <= 124 and -res >= 1) or ok;

The expected error messages are:
  24     procedure sysexit (return_code : exit_code_t) is
  25        res : long;
  26        ok  : Boolean;
  27     begin
  28        syscall1(Linux_i86.sys_exit, long(return_code), res, ok);
            ^2,3
!!! (  2)  Flow Error        : 10: Assignment to ok is ineffective.
!!! (  3)  Flow Error        : 10: Assignment to res is ineffective.

  29     end sysexit;

!!! (  4)  Flow Error        : 33: The variable res is neither referenced nor 
           exported.
!!! (  5)  Flow Error        : 33: The variable ok is neither referenced nor 
           exported.


Gna! How could I annotate, that those information has to be dropped?

Of course, there is the simple hide trick, but I do not really like it:

  24     procedure sysexit (return_code : exit_code_t) is
  25        res : long;
  26        ok  : Boolean;
  27        procedure Collect
  28          --# global in res, ok;
  29          --# derives null from res, ok;
  30          is
  31           --# hide Collect;
  32        begin
  33           null;
  34        end Collect;
  35        pragma Inline (Collect);
  36     begin
  37        syscall1(Linux_i86.sys_exit, long(return_code), res, ok);
  38        Collect;
  39     end sysexit;

+++        Flow analysis of subprogram sysexit performed: 
           no errors found.