Clarification for SPARK postconditions on hidden subprograms.

[xorque <xorquewasp@googlemail.com>]

Hello.

I'm trying to work out what should be happening regarding the
postcondition
on a function with a hidden body:

  function C_Open_Boundary
    (File_Name : in String;
     Flags     : in Open_Flag_Integer_t;
     Mode      : in Permissions.Mode_Integer_t) return Descriptor_t
  is
    --# hide C_Open_Boundary
    --# return D => (D  = -1 -> Error.Get_Error /= Error.Error_None)
or
    --#             (D /= -1 -> Error.Get_Error  = Error.Error_None);
    ...
  end C_Open_Boundary;

Is a postcondition on a hidden subprogram always assumed to have
been satisfied?

I ask because a subprogram that calls C_Open_Boundary and then
checks the return value against -1 can't seem to work out that
Error.Get_Error won't be equal to Error.Error_None when the value
is equal to -1.

Is it an error in my postcondition?

I will post more of the implementation if necessary, I just don't want
to spam the list with a 100 lines of VCGs...