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:49:00 PST Path: archiver1.google.com!news1.google.com!newsfeed.stanford.edu!news-spur1.maxwell.syr.edu!news.maxwell.syr.edu!newsfeed.frii.net!newsfeed.frii.net!news.compaq.com!uunet!sac.uu.net!ash.uu.net!lore.csc.com!baen1673807.greenlnk.net!baen1673807!not-for-mail From: "Phil Thornley" Newsgroups: comp.lang.ada Subject: Re: [Spark] How to terminate information flow? Date: Tue, 25 Mar 2003 08:49:21 -0000 Organization: Computer Sciences Corporation Message-ID: <3e801794$1@baen1673807.greenlnk.net> References: NNTP-Posting-Host: 20.44.241.70 X-Trace: lore.csc.com 1048582137 25156 20.44.241.70 (25 Mar 2003 08:48:57 GMT) X-Complaints-To: abuse@news.csc.com NNTP-Posting-Date: Tue, 25 Mar 2003 08:48:57 +0000 (UTC) X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 5.00.2919.6600 X-MimeOLE: Produced By Microsoft MimeOLE V5.00.2919.6600 X-Original-NNTP-Posting-Host: waec857.wa.bae.co.uk X-Original-Trace: 25 Mar 2003 08:47:16 GMT, waec857.wa.bae.co.uk Xref: archiver1.google.com comp.lang.ada:35671 Date: 2003-03-25T08:49:21+00:00 List-Id: "Lutz Donnerhacke" wrote in message news:slrnb7ucqt.o1.lutz@taranis.iks-jena.de... > I came across a strange situation drop loss of information and do not know > how to annotate that. [snip problem] > 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: You are right to want to avoid the use of hide. This example indicates that most non-trivial SPARK systems will have some sections of valid (correct, provable, etc.) code that generate flow errors. In your example you are coding at the SPARK boundary, and it is very common to get flow errors here. The way to deal with these is to document the fact that the flow errors will be reported and explain why they don't indicate a problem. (I believe that Praxis-CS have an idea for a mechanism for suppressing expected error reports but don't know the state of its implementation.) The usual approach at present is to add a comment to the end of the line that is echoed in the error report, such as: syscall1(Linux_i86.sys_exit, long(return_code), res, ok); -- error 10 for res and ok expected end sysexit; -- error 33 for res and ok expected Then document elsewhere (perhaps in an extended comment in the code) why the error reports don't indicate a problem. I recently came across another example of the same sort of thing. In John Barnes' Ada 95 book (second edition) there is a program called Magic_Moments (that calculates various moments of inertia for different shapes) which uses a type hierarchy for the shapes. One of the primitive subprograms is 'Name', which simply returns a string such as "Circle " or "Square ". In the SPARK version of this code, the subprogram must have its parameter (to make it primitive) but the value of the parameter isn't used so flow errors are generated. Cheers, Phil Thornley -- Phil Thornley Programmes, Engineering Warton