Re: Workaround for invariant SPARK condition

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

On 25 June, 00:03, xorque <xorquew...@googlemail.com> wrote:
> Hello.
>
> I have a piece of code that does this:
>
> function Check_Support (Request : in Request_t) return Boolean is
> begin
>   return Request /= Unsupported;
> end Check_Support;
>
> I'm using it in some code:
>
> if Check_Support (Request_Push) then
>   ...
> end if;
>
> Request_Push is a compile-time constant with an implementation-defined
> value. Given that the value is detected at compile-time, SPARK thinks
> the
> condition is invariant.
>
> Is there some way I can tell SPARK that this condition isn't actually
> invariant,
> even though it appears to be?

You could turn it into a variable, but then it would infiltrate into
all the annotations, which you probably don't want.

This is the sort of problem that the accept annotation is there for:
   --# accept F, 22, "Value is implementation defined.";
   if Check_Support (Request_Push) then
   --# end accept;

Phil Thornley