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.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD, FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: 103376,4e0df1f3e9a1ac5d X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII Path: g2news2.google.com!postnews.google.com!f35g2000vbl.googlegroups.com!not-for-mail From: Phil Thornley Newsgroups: comp.lang.ada Subject: Re: SPARK: Problem with using constants in a post annotation Date: Mon, 17 Jan 2011 07:17:11 -0800 (PST) Organization: http://groups.google.com Message-ID: References: <880b38c9-e06a-4fe5-8285-bd30a8471639@f35g2000vbl.googlegroups.com> <961b0543-de9c-4878-8370-2519e5bb01f0@l22g2000vbp.googlegroups.com> NNTP-Posting-Host: 88.97.49.112 Mime-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Trace: posting.google.com 1295277431 30007 127.0.0.1 (17 Jan 2011 15:17:11 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: Mon, 17 Jan 2011 15:17:11 +0000 (UTC) Complaints-To: groups-abuse@google.com Injection-Info: f35g2000vbl.googlegroups.com; posting-host=88.97.49.112; posting-account=Fz1-yAoAAACc1SDCr-Py2qBj8xQ-qC2q User-Agent: G2/1.0 X-HTTP-UserAgent: Mozilla/4.0 (compatible; MSIE 8.0; Windows NT 6.1; WOW64; Trident/4.0; SLCC2; .NET CLR 2.0.50727; .NET CLR 3.5.30729; .NET CLR 3.0.30729; Media Center PC 6.0; .NET4.0C),gzip(gfe) Xref: g2news2.google.com comp.lang.ada:17461 Date: 2011-01-17T07:17:11-08:00 List-Id: On Jan 17, 11:08=A0am, Mark Lorenzen 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