From: "Gavino" <invalid@invalid.invalid>
Subject: Re: Question about SPARK flow error.
Date: Sat, 19 Jun 2010 20:14:50 +0200
Date: 2010-06-19T20:14:50+02:00 [thread overview]
Message-ID: <884fp3Ft1U1@mid.individual.net> (raw)
In-Reply-To: 4c1cf6a3$0$30803$4d3efbfe@news.sover.net
"Peter C. Chapin" <pcc482719@gmail.com> wrote in message
news:4c1cf6a3$0$30803$4d3efbfe@news.sover.net...
> Am I missing something or is this reasoning outside of the abilities of
> SPARK's flow analysis? Is there some other idiomatic way I should be
handling
> this sort of situation?
Flow analysis is only concerned with syntactically possible paths through
the code and does not consider semantic aspects such as this.
For that level of analysis, you need to use the SPARK proof tools.
You could shut the Examiner up by initialising Index (eg to
Index_type'First), but it doesn't seem a satisfactory solution.
next prev parent reply other threads:[~2010-06-19 18:14 UTC|newest]
Thread overview: 9+ messages / expand[flat|nested] mbox.gz Atom feed top
2010-06-19 16:58 Question about SPARK flow error Peter C. Chapin
2010-06-19 18:03 ` Phil Thornley
2010-06-19 18:23 ` Gavino
2010-06-19 19:24 ` Phil Thornley
2010-06-19 18:14 ` Gavino [this message]
2010-06-19 19:29 ` Phil Thornley
2010-06-19 23:28 ` Phil Thornley
2010-06-20 0:37 ` Peter C. Chapin
2010-06-20 8:42 ` Phil Thornley
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox