Re: [Spark] How to terminate information flow?

["Phil Thornley" <phil.thornley@baesystems.com>]

"Lutz Donnerhacke" <lutz@iks-jena.de> 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