From: Rod Chapman <roderick.chapman@googlemail.com>
Subject: Re: SPARK - runtime checks question
Date: Fri, 19 Jun 2009 09:04:34 -0700 (PDT)
Date: 2009-06-19T09:04:34-07:00 [thread overview]
Message-ID: <aeccd921-a631-40eb-a614-343cfb338c07@q14g2000vbn.googlegroups.com> (raw)
In-Reply-To: 8d79ac48-d35d-4717-aca3-68f036de0de3@f16g2000vbf.googlegroups.com
> and of course 50% of VCs are undischarged in the final report.
The Examiner, by default, doesn't know the values of Natural'First
and Natural'Last, since these are implementation-defined.
You can supply these values with a configuration file - see
the Examiner User Manual. Run the Examiner
with the -conf switch to re-generate the VCs, then re-simplify.
I then get 100% of the VCs proved.
- Rod Chapman, SPARK Team
PS...we now always recommend the use of -vcg not -rtc
to generate VCs now.
next prev parent reply other threads:[~2009-06-19 16:04 UTC|newest]
Thread overview: 8+ messages / expand[flat|nested] mbox.gz Atom feed top
2009-06-19 15:26 SPARK - runtime checks question Maciej Sobczak
2009-06-19 15:31 ` Maciej Sobczak
2009-06-19 16:04 ` Rod Chapman [this message]
2009-06-19 18:29 ` Adam Beneschan
2009-06-19 18:55 ` Rod Chapman
2009-06-19 21:38 ` Maciej Sobczak
2009-06-19 18:33 ` Adam Beneschan
2009-06-19 21:16 ` Maciej Sobczak
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox