From: Phil Thornley <phil.jpthornley@gmail.com>
Subject: Re: task discriminants and invariant expressions in SPARK
Date: Thu, 3 Nov 2011 02:34:08 -0700 (PDT)
Date: 2011-11-03T02:34:08-07:00 [thread overview]
Message-ID: <c3cd5d68-4112-43db-9541-dd6434985b87@l19g2000yqc.googlegroups.com> (raw)
In-Reply-To: 4eae96be$0$6564$9b4e6d93@newsspool4.arcor-online.net
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
next prev parent reply other threads:[~2011-11-03 9:34 UTC|newest]
Thread overview: 5+ messages / expand[flat|nested] mbox.gz Atom feed top
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 [this message]
2011-11-03 12:11 ` Georg Bauhaus
2011-11-03 14:15 ` Georg Bauhaus
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox