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 X-Google-Attributes: gid103376,public X-Google-ArrivalTime: 2003-03-25 00:30:33 PST Path: archiver1.google.com!news1.google.com!newsfeed.stanford.edu!headwall.stanford.edu!fu-berlin.de!uni-berlin.de!213.155.153.242!not-for-mail From: Peter Amey Newsgroups: comp.lang.ada Subject: Re: [Spark] How to terminate information flow? Date: Tue, 25 Mar 2003 08:32:18 +0000 Message-ID: <3E801412.1030605@praxis-cs.co.uk> References: NNTP-Posting-Host: 213.155.153.242 Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit X-Trace: fu-berlin.de 1048581032 79904597 213.155.153.242 (16 [69815]) User-Agent: Mozilla/5.0 (Windows; U; Windows NT 5.0; en-US; rv:1.0.2) Gecko/20030208 Netscape/7.02 X-Accept-Language: en-us, en Xref: archiver1.google.com comp.lang.ada:35670 Date: 2003-03-25T08:32:18+00:00 List-Id: Lutz Donnerhacke wrote: > 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? > The short answer is that you can't make those messages go away because they are true! We do not recommend slavishly trying to eliminate all flow errors as long as the reason for them is understood. The Examiner is telling you what is _really_ happening - you have to interpret that information. What we do in these cases is: (1) Choose a good naem for the unused parameters. e.g. UnusedRes and UnusedOk. You then get a flow error "assignment to unused is ineffective" which is self-documenting. (2) Add a comment to line 29 saying "expect ineffective .... because ...". Which maintain a justifation along with the code. I do have a tentative plan for a a "justify" annotation which can be placed at the point where any flow error is produced and which will suppress it at that point but add it to a summary file of justified errors. Peter