From: Mark Lorenzen <mark.lorenzen@gmail.com>
Subject: Re: SPARK: Problem with using constants in a post annotation
Date: Mon, 17 Jan 2011 03:08:04 -0800 (PST)
Date: 2011-01-17T03:08:04-08:00 [thread overview]
Message-ID: <961b0543-de9c-4878-8370-2519e5bb01f0@l22g2000vbp.googlegroups.com> (raw)
In-Reply-To: 880b38c9-e06a-4fe5-8285-bd30a8471639@f35g2000vbl.googlegroups.com
On 13 Jan., 12:15, Phil Thornley <phil.jpthorn...@gmail.com> wrote:
>
> BUT - there is an defect in the current (ie GPL 2010) version of SPARK
> where this may generate incorrect VCs for Proc. This seems to occur
> when a pre- and/or post-condition is refined but there is no refined
> information flow (ie the derives annotation). I don't know of any
> reliable workaround for this.
> (I understand that the SPARK team have fixed this defect, so if you
> are a supported customer you should be able to get an updated
> Examiner.)
>
It would be really nice if AdaCore would issue an update to the GPL
version as well. I understand they can't update the GPL version every
time they issue a new wavefront release of a supported product, but
this bug has no workaround and it gives a bad impression of SPARK.
- Mark L
next prev parent reply other threads:[~2011-01-17 11:08 UTC|newest]
Thread overview: 8+ messages / expand[flat|nested] mbox.gz Atom feed top
2011-01-13 9:18 SPARK: Problem with using constants in a post annotation George
2011-01-13 9:26 ` George
2011-01-13 11:15 ` Phil Thornley
2011-01-13 12:23 ` George
2011-01-17 11:08 ` Mark Lorenzen [this message]
2011-01-17 15:17 ` Phil Thornley
2011-01-17 16:13 ` Mark Lorenzen
2011-01-13 11:15 ` George
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox