Re: Clarification for SPARK postconditions on hidden subprograms.

[Phil Thornley <phil.jpthornley@googlemail.com>]

On 26 June, 10:29, xorque <xorquew...@googlemail.com> wrote:
[...]
> Moving the annotation has, of course, highlighted an apparent error
> on my part:
>
>   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.
>
>   83      --#      ((Descriptor /= -1) -> (Error.Get_Error  =
> Error.Error_None));
>                                            ^
> ***        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.

But this isn't a parameterless function - it must have a global
annotation, something like:
function Error return Error_T;
--# global Stored_Error;

in which case the *proof* function Error has a parameter corresponding
to the global Stored_Error.
(Proof functions are not allowed global access to anything.)

Phil Thornley