From: Phil Thornley <phil.jpthornley@gmail.com>
Subject: Re: SPARK: Problem with using constants in a post annotation
Date: Mon, 17 Jan 2011 07:17:11 -0800 (PST)
Date: 2011-01-17T07:17:11-08:00 [thread overview]
Message-ID: <b5e815ae-658c-4c86-8b2d-e91b11422b82@f35g2000vbl.googlegroups.com> (raw)
In-Reply-To: 961b0543-de9c-4878-8370-2519e5bb01f0@l22g2000vbp.googlegroups.com
On Jan 17, 11:08 am, Mark Lorenzen <mark.loren...@gmail.com> wrote:
[...]
> 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.
Looks like this wish has been answered. Adacore have just announced a
new version of SPARK GPL.
The main change is the preview of the SPARKBridge technology which
allows SMT solvers to be used along with the Simplifier. The release
note says that this error in VC generation has been fixed.
Cheers,
Phil
next prev parent reply other threads:[~2011-01-17 15:17 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
2011-01-17 15:17 ` Phil Thornley [this message]
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