Representing errno in SPARK

[xorquewasp@googlemail.com]

What is the correct way to model a pair of subprograms
that affect state completely outside of the SPARK program?

Specifically, in this case, I have a procedure:

  procedure Errno_Set (Code : Integer);
  pragma Import (C, Errno_Set, "posix_errno_set");

And a function:

  function Errno_Get return Integer;
  pragma Import (C, Errno_Get, "posix_errno_get");

The problem in this case is that the C variable 'errno' that these
subprograms refer to is completely external to the program but
the value of the Errno_Get function depends on it and therefore
the execution path the program takes depends on it. Those
closest I can find in the SPARK95 manual is "external own variables"
but even then, the variables are actually objects within the program:

package body Device
--# own State is        OldX,       -- state variable constituent
--#              in     StatusPort, -- external variable constituent
--#                 out Register;   -- external variable constituent
is
  OldX : Integer := 0; -- only component that needs or permits
initialization

  StatusPort : Integer;
  for StatusPort’Address use .........;
  Register : Integer;
  for Register’Address use ..........;