From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=0.4 required=5.0 tests=BAYES_00,FORGED_MUA_MOZILLA
	autolearn=no autolearn_force=no version=3.4.4
X-Google-Thread: 103376,c0b40cfe80587a8d,start
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Received: by 10.205.116.5 with SMTP id fg5mr1766486bkc.3.1320064786804;
        Mon, 31 Oct 2011 05:39:46 -0700 (PDT)
Path: 
 l23ni33563bkv.0!nntp.google.com!news2.google.com!news3.google.com!feeder1-2.proxad.net!proxad.net!feeder2-2.proxad.net!newsfeed.arcor.de!newsspool3.arcor-online.net!news.arcor.de.POSTED!not-for-mail
Date: Mon, 31 Oct 2011 13:38:21 +0100
From: Georg Bauhaus <rm.dash-bauhaus@futureapps.de>
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6;
 rv:7.0.1) Gecko/20110929 Thunderbird/7.0.1
MIME-Version: 1.0
Newsgroups: comp.lang.ada
Subject: [Q] task discriminants and invariant expressions in SPARK
Message-ID: <4eae96be$0$6564$9b4e6d93@newsspool4.arcor-online.net>
Organization: Arcor
NNTP-Posting-Date: 31 Oct 2011 13:38:22 CET
NNTP-Posting-Host: 8ea6889e.newsspool4.arcor-online.net
X-Trace: 
 DXC=_105ekKNWW\5TOT9_N5i<V4IUK<Cl32<Q4Fo<]lROoRQ8kF<OcfhCO[i^]>]GbD7b_PCY\c7>ejVX3;GGVR0\5_^51dTiX2?NM_
X-Complaints-To: usenet-abuse@arcor.de
Xref: news2.google.com comp.lang.ada:14254
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Date: 2011-10-31T13:38:22+01:00
List-Id: <comp.lang.ada>

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.