* Workaround for invariant SPARK condition
@ 2009-06-24 23:03 xorque
2009-06-25 7:48 ` Phil Thornley
0 siblings, 1 reply; 4+ messages in thread
From: xorque @ 2009-06-24 23:03 UTC (permalink / raw)
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?
^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: Workaround for invariant SPARK condition
2009-06-24 23:03 Workaround for invariant SPARK condition xorque
@ 2009-06-25 7:48 ` Phil Thornley
2009-06-25 8:50 ` Rod Chapman
0 siblings, 1 reply; 4+ messages in thread
From: Phil Thornley @ 2009-06-25 7:48 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: Workaround for invariant SPARK condition
2009-06-25 7:48 ` Phil Thornley
@ 2009-06-25 8:50 ` Rod Chapman
2009-06-25 11:19 ` xorque
0 siblings, 1 reply; 4+ messages in thread
From: Rod Chapman @ 2009-06-25 8:50 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 4+ messages in thread
* Re: Workaround for invariant SPARK condition
2009-06-25 8:50 ` Rod Chapman
@ 2009-06-25 11:19 ` xorque
0 siblings, 0 replies; 4+ messages in thread
From: xorque @ 2009-06-25 11:19 UTC (permalink / raw)
Thanks.
I wasn't aware of the accept annotation.
^ permalink raw reply [flat|nested] 4+ messages in thread
end of thread, other threads:[~2009-06-25 11:19 UTC | newest]
Thread overview: 4+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2009-06-24 23:03 Workaround for invariant SPARK condition xorque
2009-06-25 7:48 ` Phil Thornley
2009-06-25 8:50 ` Rod Chapman
2009-06-25 11:19 ` xorque
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox