* [Q] task discriminants and invariant expressions in SPARK
@ 2011-10-31 12:38 Georg Bauhaus
2011-10-31 13:04 ` Georg Bauhaus
2011-11-03 9:34 ` Phil Thornley
0 siblings, 2 replies; 5+ messages in thread
From: Georg Bauhaus @ 2011-10-31 12:38 UTC (permalink / raw)
In a subprogram (named Test) local to a task, the body is a case
distinction that depends only on the value of the task's discriminant.
SPARK reports a flow error because referring to the discriminant
yields an invariant expression. I am trying to understand why
this is a flow error. Or maybe, why this flow is an error. I see
that for invariant expression of a case statement, only one of
the branches of the case statement will be computed per task
subtype, and that the discriminant will have a statically know value.
(I couldn't think of an easy workaround but that may be just me.)
Additionally, will the same flow error be reported for case expressions
or---by extension of the argument---for expression functions?
package Tsk
--# own task Busy : Business;
--# protected Data : Binary;
is
type Binary is mod 2**8;
pragma Atomic (Binary);
type Name is (Fred, Barney);
task type Business (Id : Name)
--# global in out Data;
--# derives Data from Data; -- , Id (constant, not entire_variable)
is
pragma Priority (5);
end Business;
end tsk;
package body Tsk is
Data : Binary := 2#0#;
subtype Freds_Business is Business (Id => Fred);
Busy : Freds_Business;
task body Business is
Current_Data : Binary;
procedure Test
--# global out Data;
--# derives Data from ;
is
begin
case Id is
when Fred =>
Data := 2#1#;
when Barney =>
Data := 2#101#;
end case;
end Test;
begin
loop
Current_Data := Data;
if Current_Data = 2#0# then
Test;
end if;
end loop;
end Business;
end Tsk;
Examining the body of package Tsk ...
18 case Id is
^
!!! Flow Error : 22: Value of expression is invariant.
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: [Q] task discriminants and invariant expressions in SPARK
2011-10-31 12:38 [Q] task discriminants and invariant expressions in SPARK Georg Bauhaus
@ 2011-10-31 13:04 ` Georg Bauhaus
2011-11-03 9:34 ` Phil Thornley
1 sibling, 0 replies; 5+ messages in thread
From: Georg Bauhaus @ 2011-10-31 13:04 UTC (permalink / raw)
On 31.10.11 13:38, Georg Bauhaus wrote:
> (I couldn't think of an easy workaround but that may be just me.)
Apparently, the following seem to be o.K., no more flow error,
but is it cheating?
procedure Test (V : Name) ...
... case V is ...
Test (Id);
Just one indirection...
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: task discriminants and invariant expressions in SPARK
2011-10-31 12:38 [Q] task discriminants and invariant expressions in SPARK Georg Bauhaus
2011-10-31 13:04 ` Georg Bauhaus
@ 2011-11-03 9:34 ` Phil Thornley
2011-11-03 12:11 ` Georg Bauhaus
1 sibling, 1 reply; 5+ messages in thread
From: Phil Thornley @ 2011-11-03 9:34 UTC (permalink / raw)
On Oct 31, 12:38 pm, Georg Bauhaus <rm.dash-bauh...@futureapps.de>
wrote:
> In a subprogram (named Test) local to a task, the body is a case
> distinction that depends only on the value of the task's discriminant.
> SPARK reports a flow error because referring to the discriminant
> yields an invariant expression. I am trying to understand why
> this is a flow error. Or maybe, why this flow is an error.
I can't find anything relevant in the documentation - there's no list
of known deficiences in the GPL release note.
It is probably worth reporting this even if you are not a supported
customer - use spark@adacore.com as the address (and include "SPARK"
in the subject line otherwise it gets dumped in the spam bucket).
Cheers,
Phil
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: task discriminants and invariant expressions in SPARK
2011-11-03 9:34 ` Phil Thornley
@ 2011-11-03 12:11 ` Georg Bauhaus
2011-11-03 14:15 ` Georg Bauhaus
0 siblings, 1 reply; 5+ messages in thread
From: Georg Bauhaus @ 2011-11-03 12:11 UTC (permalink / raw)
On 03.11.11 10:34, Phil Thornley wrote:
> I can't find anything relevant in the documentation - there's no list
> of known deficiences in the GPL release note.
>
> It is probably worth reporting this even if you are not a supported
> customer - use spark@adacore.com as the address (and include "SPARK"
> in the subject line otherwise it gets dumped in the spam bucket).
Thanks for having a look. A report is now sent.
I have also tried a variation that uses a protected object
in place of an atomic object. Same diagnostic message.
^ permalink raw reply [flat|nested] 5+ messages in thread
* Re: task discriminants and invariant expressions in SPARK
2011-11-03 12:11 ` Georg Bauhaus
@ 2011-11-03 14:15 ` Georg Bauhaus
0 siblings, 0 replies; 5+ messages in thread
From: Georg Bauhaus @ 2011-11-03 14:15 UTC (permalink / raw)
On 03.11.11 13:11, Georg Bauhaus wrote:
> On 03.11.11 10:34, Phil Thornley wrote:
>
>> I can't find anything relevant in the documentation - there's no list
>> of known deficiences in the GPL release note.
>>
>> It is probably worth reporting this even if you are not a supported
>> customer - use spark@adacore.com as the address (and include "SPARK"
>> in the subject line otherwise it gets dumped in the spam bucket).
>
> Thanks for having a look. A report is now sent.
I've got a reply! Both, discriminant-is-constant and
discriminant-turned-variable through making it a parameter
would be expected in the current RavenSPARK model, and
deliberately. Good to know.
^ permalink raw reply [flat|nested] 5+ messages in thread
end of thread, other threads:[~2011-11-03 14:15 UTC | newest]
Thread overview: 5+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2011-10-31 12:38 [Q] task discriminants and invariant expressions in SPARK Georg Bauhaus
2011-10-31 13:04 ` Georg Bauhaus
2011-11-03 9:34 ` Phil Thornley
2011-11-03 12:11 ` Georg Bauhaus
2011-11-03 14:15 ` Georg Bauhaus
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox