Re: [Spark] How to terminate information flow?

[Peter Amey <peter.amey@praxis-cs.co.uk>]

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