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=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM
	autolearn=ham autolearn_force=no version=3.4.4
X-Google-Thread: a07f3367d7,1bf4286a3f0b5d7e
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news2.google.com!postnews.google.com!c19g2000yqc.googlegroups.com!not-for-mail
From: roderick.chapman@googlemail.com
Newsgroups: comp.lang.ada
Subject: Re: SPARK postcondition check fails
Date: Mon, 8 Jun 2009 23:45:14 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: 
 <5a1a9746-2893-4c2e-a1b7-6107d33f2524@c19g2000yqc.googlegroups.com>
References: 
 <02cc303d-6a22-4f09-b174-d2fbbb422645@t10g2000vbg.googlegroups.com>
NNTP-Posting-Host: 192.108.117.69
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 7bit
X-Trace: posting.google.com 1244529914 31354 127.0.0.1 (9 Jun 2009 06:45:14
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Tue, 9 Jun 2009 06:45:14 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: c19g2000yqc.googlegroups.com; posting-host=192.108.117.69;
	posting-account=HCzrEgkAAABSfGsTnv-u5wET6EzuneVi
User-Agent: G2/1.0
X-HTTP-UserAgent: Mozilla/5.0 (Windows; U; Windows NT 5.1; en-GB;
 rv:1.9.0.10)
	Gecko/2009042316 Firefox/3.0.10,gzip(gfe),gzip(gfe)
Xref: g2news2.google.com comp.lang.ada:6383
Date: 2009-06-08T23:45:14-07:00
List-Id: <comp.lang.ada>

> You'll have to forgive the possibly naive question, there's quite
> a learning curve.

Habe you run the Simplifier over the generated VCs?

The Examiner _generates_ the VCs, but you need to run "sparksimp"
to Simplify them, then "pogs" to collate the results.  Please see
chapter 10 of the SPARK book, or the Tokeneer Discovery tutorial
for more details.
 - Rod Chapman