Re: Representing errno in SPARK

[Phil Thornley <phil.jpthornley@googlemail.com>]

On Jun 9, 4:02 pm, xorquew...@googlemail.com wrote:
...
>
> Thank you, that's actually what I have here. The problem, however,
> is that the package also has a body and SPARK doesn't seem to
> like this:
>
> $ spark posix-error.ads posix-error.adb
> ...
>  304  end POSIX.Error;
>           ^
> ***        Semantic Error    : 28: The own variable POSIX_errno does
> not have a
>            definition [SR95 7.2.3].
>
> Is it, by any chance, an issue due to Errno_Get and Errno_Set being
> defined in the private section of the package spec? I think probably
> not...

No it's not that.

What you are trying to do (by having other SPARK code in the body) is
mixing code that is inside and outside the 'SPARK boundary' in a
single package.

One possibility is to move the Errno abstraction and the two imported
operations to another package internal to POSIX (but this means having
an implementation for the POSIX versions of these subprograms). So:

1 - Remove the Import pragmas from POSIX spec.
2 - Create an internal package (eg POSIX.Internals) in the POSIX body
that has the Errno abstraction and the imported subprograms.
3 - In the refinement annotation on the POSIX body put "--# own Errno
is Internals.Errno;".
4 - Call through to these imported subprograms in the implementation
of the subprograms that you now have to provide.

(A second possibility is simply to create an Errno in the package body
with a comment that it isn't actually used by the code ...)

Phil Thornley