[Q] task discriminants and invariant expressions in SPARK

[Georg Bauhaus <rm.dash-bauhaus@futureapps.de>]

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.