Re: Clarification for SPARK postconditions on hidden subprograms.

[Rod Chapman <roderick.chapman@googlemail.com>]

On Jun 26, 10:29 am, xorque <xorquew...@googlemail.com> wrote:
>   82      --# post ((Descriptor  = -1) -> (Error.Get_Error /=
> Error.Error_None)) or
>                                            ^
> ***        Semantic Error    :  3: Incorrect number of actual
> parameters for call
>            of subprogram Get_Error.
> Does SPARK take issue with parameterless functions? Not unreasonable
> at all if this is the case, as SPARK should probably see them as
> constants.

Does this function have a global variable by any chance? If so, then
in annotations, you have to give additional actual parameters.
See section 3.3 of the Examiner_GenVCs manual.

> I hadn't made the connection until just now that you were the
> author of those. Thanks for writing those - there's a distinct lack
> of SPARK related info online.

We have very deliberately made the _entire_ set of manuals
available with the GPL release.  We hope in future to make
more tutorial-style information available on-line.

Yours,
 Rod Chapman, SPARK Team