SPARK parameter type error.

SPARK parameter type error.

[xorquewasp]

Hello.

I've run up against another odd SPARK examiner error.

The two troublesome packages are as follows:

package POSIX.Error
  --# own POSIX_errno;
is

  type Error_t is
    (Error_None,
     Error_Access,
     Error_Unknown);

  --
  -- Map error value to locale-specific error message.
  --

  procedure Message
    (Value  : in Error_t;
     Buffer : out String);
  --# derives Buffer from Value;

  --
  -- Get current error code.
  --

  function Get_Error return Error_t;
  --# global in POSIX_errno;

private

  Errno_Int_Size : constant Positive := 32;
  type Errno_Int_t is range -2147483647 .. 2147483647;
  for Errno_Int_t'Size use Errno_Int_Size;
  pragma Convention (C, Errno_Int_t);

  --
  -- Mapping between errno and Ada error codes.
  --

  function Ada_To_Errno (Value : in Error_t) return Errno_Int_t;
  function Errno_To_Ada (Value : in Errno_Int_t) return Error_t;

  --
  -- Return POSIX errno integer.
  --

  function Errno_Get return Errno_Int_t;
  --# global in POSIX_errno;
  pragma Import (C, Errno_Get, "posix_errno_get");

  --
  -- Set POSIX errno integer.
  --

  procedure Errno_Set (Code : in Errno_Int_t);
  --# global out POSIX_Errno;
  --# derives POSIX_Errno from Code;
  pragma Import (C, Errno_Set, "posix_errno_set");

end POSIX.Error;

with POSIX.Error;
with POSIX.Permissions;
with System;

--# inherit POSIX.Error,
--#         POSIX.Permissions,
--#         System;

package POSIX.File is

  Descriptor_Size : constant Positive := 32;
  type Descriptor_t is range -1 .. 2147483647;
  for Descriptor_t'Size use Descriptor_Size;
  pragma Convention (C, Descriptor_t);

  type Flags_t is mod 2 ** 32;

  procedure Open_Read_Only
    (File_Name    : in String;
     Non_Blocking : in Boolean;
     Descriptor   : out Descriptor_t;
     Error_Value  : out POSIX.Error.Error_t);
  --# derives Descriptor, Error_Value from File_Name, Non_Blocking;

  procedure Open_Write_Only
    (File_Name    : in String;
     Non_Blocking : in Boolean;
     Descriptor   : out Descriptor_t;
     Error_Value  : out POSIX.Error.Error_t);
  --# derives Descriptor, Error_Value from File_Name, Non_Blocking;

  procedure Open_Exclusive
    (File_Name    : in String;
     Non_Blocking : in Boolean;
     Mode         : in Permissions.Mode_t;
     Descriptor   : out Descriptor_t;
     Error_Value  : out POSIX.Error.Error_t);
  --# derives Descriptor, Error_Value from File_Name, Non_Blocking,
Mode;

  procedure Open_Append
    (File_Name    : in String;
     Non_Blocking : in Boolean;
     Descriptor   : out Descriptor_t;
     Error_Value  : out POSIX.Error.Error_t);
  --# derives Descriptor, Error_Value from File_Name, Non_Blocking;

  procedure Open_Truncate
    (File_Name    : in String;
     Non_Blocking : in Boolean;
     Mode         : in Permissions.Mode_t;
     Descriptor   : out Descriptor_t;
     Error_Value  : out POSIX.Error.Error_t);
  --# derives Descriptor, Error_Value from File_Name, Non_Blocking,
Mode;

  procedure Open_Read_Write
    (File_Name    : in String;
     Non_Blocking : in Boolean;
     Descriptor   : out Descriptor_t;
     Error_Value  : out POSIX.Error.Error_t);
  --# derives Descriptor, Error_Value from File_Name, Non_Blocking;

  procedure Open_Create
    (File_Name    : in String;
     Non_Blocking : in Boolean;
     Mode         : in Permissions.Mode_t;
     Descriptor   : out Descriptor_t;
     Error_Value  : out POSIX.Error.Error_t);
  --# derives Descriptor, Error_Value from File_Name, Non_Blocking,
Mode;

  procedure Open
    (File_Name    : in String;
     Non_Blocking : in Boolean;
     Mode         : in Permissions.Mode_t;
     Flags        : in Flags_t;
     Descriptor   : out Descriptor_t;
     Error_Value  : out POSIX.Error.Error_t);
  --# derives Descriptor, Error_Value from File_Name, Non_Blocking,
Mode, Flags;

  Append     : constant Flags_t;
  Create     : constant Flags_t;
  Exclusive  : constant Flags_t;
  Read_Only  : constant Flags_t;
  Read_Write : constant Flags_t;
  Truncate   : constant Flags_t;
  Write_Only : constant Flags_t;

private

  O_RDONLY   : constant Flags_t := 16#0#;
  O_WRONLY   : constant Flags_t := 16#1#;
  O_NONBLOCK : constant Flags_t := 16#800#;
  O_APPEND   : constant Flags_t := 16#400#;
  O_CREAT    : constant Flags_t := 16#40#;
  O_EXCL     : constant Flags_t := 16#80#;
  O_TRUNC    : constant Flags_t := 16#200#;

  Append     : constant Flags_t := O_APPEND;
  Create     : constant Flags_t := O_CREAT;
  Exclusive  : constant Flags_t := O_EXCL;
  Read_Only  : constant Flags_t := O_RDONLY;
  Read_Write : constant Flags_t := O_RDONLY or O_WRONLY;
  Truncate   : constant Flags_t := O_TRUNC;
  Write_Only : constant Flags_t := O_WRONLY;

  function C_Open
    (File_Name : in System.Address;
     Flags     : in Flags_t;
     Mode      : in Permissions.Mode_t) return Descriptor_t;
  pragma Import (C, C_Open, "open");

end POSIX.File;

Running spark on posix-file.ads results in many instances of:

  42       Error_Value  : out POSIX.Error.Error_t);
                                    ^
***        Semantic Error    :754: The identifier Error is either
undeclared or not
           visible at this point. This package must be both inherited
and
           withed to be visible here.

The index file is correctly written:

POSIX             spec is in posix.ads
POSIX.Error       spec is in posix-error.ads
POSIX.Error       body is in posix-error.adb
POSIX.File        spec is in posix-file.ads
POSIX.File        body is in posix-file.adb
POSIX.Permissions spec is in posix-permissions.ads

I thought perhaps that it was something to do with the way the
parameter
type was specified. Having tried a more minimal example, however:

package pkg2 is

  type p2_type is range 1 .. 20;

end pkg2;

with pkg2;

--# inherit pkg2;

package pkg1 is

  procedure Init (X : out pkg2.p2_type);
  --# derives X from;

end pkg1;

Results in no errors.

What's going on?

Re: SPARK parameter type error.

[Phil Thornley]

> Running spark on posix-file.ads results in many instances of:
>
>   42       Error_Value  : out POSIX.Error.Error_t);
>                                     ^
> ***        Semantic Error    :754: The identifier Error is either
> undeclared or not
>            visible at this point. This package must be both inherited
> and
>            withed to be visible here.
>

> What's going on?

The SPARK language doesn't allow the optional (in Ada) parent name to
be given - so just delete all the POSIX. prefixes and it will work.

(SPARK insists that any entity can only have a single name - in this
case Error.Error_t - and disallows POSIX.Error.Error_t).

Cheers,

Phil Thornley

Re: SPARK parameter type error.

[xorquewasp]

Phil Thornley wrote:
>
> The SPARK language doesn't allow the optional (in Ada) parent name to
> be given - so just delete all the POSIX. prefixes and it will work.
>
> (SPARK insists that any entity can only have a single name - in this
> case Error.Error_t - and disallows POSIX.Error.Error_t).

Thanks.

Wasn't aware that unique meant quite *that* unique!