[Q] task discriminants and invariant expressions in SPARK

[Q] task discriminants and invariant expressions in SPARK

[Georg Bauhaus]

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.

Re: [Q] task discriminants and invariant expressions in SPARK

[Georg Bauhaus]

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...

Re: task discriminants and invariant expressions in SPARK

[Phil Thornley]

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

Re: task discriminants and invariant expressions in SPARK

[Georg Bauhaus]

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.

Re: task discriminants and invariant expressions in SPARK

[Georg Bauhaus]

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.