[Spark] How to terminate information flow?

[Spark] How to terminate information flow?

[Lutz Donnerhacke]

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.

Re: [Spark] How to terminate information flow?

[Peter Amey]

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

Re: [Spark] How to terminate information flow?

[Lutz Donnerhacke]

* Peter Amey wrote:
> 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.

Ok, understood.

> 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.

Done.

> (2) Add a comment to line 29 saying "expect ineffective .... because ...".
>     Which maintain a justifation along with the code.

I add a comment type (--! regex) which can be parsed automatically, in order
to suppress the examiner output on this cases by a wrapper script. This
wrapper script is even necessary here to provide a editor friendly output.
I'll put the wrapper script at
  ftp://ftp.iks-jena.de/pub/mitarb/lutz/ada/spark/spark.pl
in a few hours.

> 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.

That would be fine, but hat very low priority. A practial workaround exists.

Re: [Spark] How to terminate information flow?

[Phil Thornley]

"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