Workaround for invariant SPARK condition

Workaround for invariant SPARK condition

[xorque]

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?

Re: Workaround for invariant SPARK condition

[Phil Thornley]

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

Re: Workaround for invariant SPARK condition

[Rod Chapman]

On Jun 25, 8:48 am, Phil Thornley <phil.jpthorn...@googlemail.com>
wrote:
> This is the sort of problem that the accept annotation is there for:

Exactly.  Please see section 9.1 of the Examiner User Manual for
more details.
 Rod, SPARK Team

Re: Workaround for invariant SPARK condition

[xorque]

Thanks.

I wasn't aware of the accept annotation.