From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham
	autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 103376,d0fb3b725598ca25,start
X-Google-Attributes: gid103376,public
X-Google-ArrivalTime: 2003-03-24 08:33:39 PST
Path: 
 archiver1.google.com!news1.google.com!newsfeed.stanford.edu!news-spur1.maxwell.syr.edu!news.maxwell.syr.edu!newsfeed.icl.net!newsfeed.fjserv.net!news-FFM2.ecrc.net!news.iks-jena.de!not-for-mail
From: Lutz Donnerhacke <lutz@iks-jena.de>
Newsgroups: comp.lang.ada
Subject: [Spark] How to terminate information flow?
Date: Mon, 24 Mar 2003 16:33:38 +0000 (UTC)
Organization: IKS GmbH Jena
Message-ID: <slrnb7ucqt.o1.lutz@taranis.iks-jena.de>
NNTP-Posting-Host: taranis.iks-jena.de
X-Trace: branwen.iks-jena.de 1048523618 4122 217.17.192.37 (24 Mar 2003
 16:33:38 GMT)
X-Complaints-To: usenet@iks-jena.de
NNTP-Posting-Date: Mon, 24 Mar 2003 16:33:38 +0000 (UTC)
User-Agent: slrn/0.9.7.4 (Linux)
Xref: archiver1.google.com comp.lang.ada:35652
Date: 2003-03-24T16:33:38+00:00
List-Id: <comp.lang.ada>

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.