SPARK postcondition check fails

SPARK postcondition check fails

[xorquewasp]

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.

Re: SPARK postcondition check fails

[roderick.chapman]

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

Habe you run the Simplifier over the generated VCs?

The Examiner _generates_ the VCs, but you need to run "sparksimp"
to Simplify them, then "pogs" to collate the results.  Please see
chapter 10 of the SPARK book, or the Tokeneer Discovery tutorial
for more details.
 - Rod Chapman

Re: SPARK postcondition check fails

[xorquewasp]

On Jun 9, 7:45 am, roderick.chap...@googlemail.com wrote:
> > You'll have to forgive the possibly naive question, there's quite
> > a learning curve.
>
> Habe you run the Simplifier over the generated VCs?
>
> The Examiner _generates_ the VCs, but you need to run "sparksimp"
> to Simplify them, then "pogs" to collate the results.  Please see
> chapter 10 of the SPARK book, or the Tokeneer Discovery tutorial
> for more details.
>  - Rod Chapman

No, I hadn't.

I actually wasn't aware of the existence of the Tokeneer tutorial.
I'll be going through that ASAP.

By the SPARK book, do you mean High Integrity Ada by John Barnes?

Thanks.

Re: SPARK postcondition check fails

[roderick.chapman]

On Jun 9, 8:12 am, xorquew...@googlemail.com wrote:
> On Jun 9, 7:45 am, roderick.chap...@googlemail.com wrote:
>
> > > You'll have to forgive the possibly naive question, there's quite
> > > a learning curve.
>
> > Habe you run the Simplifier over the generated VCs?
>
> > The Examiner _generates_ the VCs, but you need to run "sparksimp"
> > to Simplify them, then "pogs" to collate the results.  Please see
> > chapter 10 of the SPARK book, or the Tokeneer Discovery tutorial
> > for more details.
> >  - Rod Chapman
>
> No, I hadn't.
>
> I actually wasn't aware of the existence of the Tokeneer tutorial.
> I'll be going through that ASAP.
>
> By the SPARK book, do you mean High Integrity Ada by John Barnes?
>
> Thanks.

It's High Integrity _Software_ - the one with the blue cover
published in 2003 (but now in its 4th re-print...)  Get it
from amazon.co.uk.
 - Rod