SPARK postcondition check fails

[xorquewasp@googlemail.com]

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.