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-Thread: a07f3367d7,1bf4286a3f0b5d7e,start
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news2.google.com!postnews.google.com!t10g2000vbg.googlegroups.com!not-for-mail
From: xorquewasp@googlemail.com
Newsgroups: comp.lang.ada
Subject: SPARK postcondition check fails
Date: Mon, 8 Jun 2009 21:55:14 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: 
 <02cc303d-6a22-4f09-b174-d2fbbb422645@t10g2000vbg.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 1244523314 1520 127.0.0.1 (9 Jun 2009 04:55:14
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Tue, 9 Jun 2009 04:55:14 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: t10g2000vbg.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:6382
Date: 2009-06-08T21:55:14-07:00
List-Id: <comp.lang.ada>

Hi.

I have the following procedure definition that I'm checking with
'spark -vcg posix-file.adb':

  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 Error.Error_t);
  --# global in Error.POSIX_errno;
  --# derives Descriptor from File_Name, Non_Blocking, Mode, Flags &
  --#         Error_Value from File_Name, Non_Blocking, Mode, Flags,
Error.POSIX_errno;
  --# post ((Descriptor >= 0) and (Error_Value = Error.Error_None)) or
  --#      ((Descriptor = -1) and (Error_Value /= Error.Error_None));


  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 Error.Error_t)
  is
    C_Flags     : Flags_t;
    C_File_Name : File_Name_t := File_Name_t'(File_Name_Index_t =>
Character'Val (0));
  begin
    -- Reject long filename.
    if File_Name'Last >= File_Name_t'Last then
      Descriptor  := -1;
      Error_Value := Error.Error_Name_Too_Long;
    else
      -- Set flags for non-blocking.
      if Non_Blocking then
        C_Flags := Flags or O_NONBLOCK;
      else
        C_Flags := Flags;
      end if;

      -- Copy and null-terminate filename.
      for Index in Positive range File_Name'First .. File_Name'Last
loop
        C_File_Name (Index) := File_Name (Index);
      end loop;
      C_File_Name (File_Name'Last + 1) := Character'Val (0);

      -- Call system open() procedure.
      Descriptor := C_Open_Boundary
        (File_Name => C_File_Name,
         Flags     => C_Flags,
         Mode      => Mode);
      if Descriptor = -1 then
        Error_Value := Error.Get_Error;
      else
        Error_Value := Error.Error_None;
      end if;
    end if;
  end Open;

The postcondition is intended to state "if Descriptor is greater than
equal to 0 after the procedure returns, Error_Value will be set to
Error.Error_None otherwise if Descriptor is equal to -1 after the
procedure returns, Error_Value will be set to a value other than
Error.Error_None".

The problem is that in the first 'if' statement where Descriptor is
set to -1 if the filename length check fails, if I modify the code to
set Descriptor to 0, SPARK doesn't notice that the procedure no
longer satisfies the postcondition on that execution path. No
warning or error is printed.

Is this a SPARK issue or an issue with the way I've specified the
postcondition?

You'll have to forgive the possibly naive question, there's quite
a learning curve.