Re: Representing errno in SPARK

[xorquewasp@googlemail.com]

roderick.chap...@googlemail.com wrote:
> Create an abstraction of that state as a SPARK abstract own
> variable, thus:
>
> package POSIX
> --# own Errno;
>
>   procedure Errno_Set (Code : Integer);
>   --# global out Errno;
>   --# derives Errno from Code;
>   pragma Import (C, Errno_Set, "posix_errno_set");
>
>   function Errno_Get return Integer;
>   --# global in Errno;
>   pragma Import (C, Errno_Get, "posix_errno_get");
>
> end POSIX;

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

>
> 2) do NOT use an external own variable for this - these
> are for _volatile_ states, which Errno is not...

Ok.

>
> 3) You should read the "Informed Design Method" manual
> (Informed.pdf) that comes with the SPARK distibution.
>

That's where I first got the idea for the above. The device
driver example in the SPARK95 manual made me think my
solution was incorrect, however.