From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM autolearn=ham autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news2.google.com!postnews.google.com!q14g2000vbn.googlegroups.com!not-for-mail From: xorquewasp@googlemail.com Newsgroups: comp.lang.ada Subject: SPARK parameter type error. Date: Mon, 8 Jun 2009 01:15:20 -0700 (PDT) Organization: http://groups.google.com Message-ID: <042da3b7-6571-49b2-926f-3a8a578437db@q14g2000vbn.googlegroups.com> NNTP-Posting-Host: 81.86.41.187 Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit X-Trace: posting.google.com 1244448920 10242 127.0.0.1 (8 Jun 2009 08:15:20 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Mon, 8 Jun 2009 08:15:20 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: q14g2000vbn.googlegroups.com; posting-host=81.86.41.187; posting-account=D9GNUgoAAAAmg7CCIh9FhKHNAJmHypsp User-Agent: G2/1.0 X-HTTP-UserAgent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.9.0.7) Gecko/2009030814 Iceweasel/3.0.9 (Debian-3.0.9-1),gzip(gfe),gzip(gfe) Xref: g2news2.google.com comp.lang.ada:6364 Date: 2009-06-08T01:15:20-07:00 List-Id: 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?