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 autolearn=ham
	autolearn_force=no version=3.4.4
X-Google-Thread: 103376,c3f4071dbfa958f
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Path: 
 g2news2.google.com!news1.google.com!news.glorb.com!feeder.erje.net!news.musoftware.de!wum.musoftware.de!fu-berlin.de!uni-berlin.de!individual.net!not-for-mail
From: "Gavino" <invalid@invalid.invalid>
Newsgroups: comp.lang.ada
Subject: Re: Question about SPARK flow error.
Date: Sat, 19 Jun 2010 20:14:50 +0200
Message-ID: <884fp3Ft1U1@mid.individual.net>
References: <4c1cf6a3$0$30803$4d3efbfe@news.sover.net>
X-Trace: individual.net 5HGiChbuCtl681HDv+QtLQM2zzEJbahEyq788OHzPPReMS90LT
Cancel-Lock: sha1:qDkcP3uOPrjk6a2Y15E3BSGPGzU=
X-Priority: 3
X-MSMail-Priority: Normal
X-Newsreader: Microsoft Outlook Express 6.00.2800.1106
X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2800.1106
Xref: g2news2.google.com comp.lang.ada:12792
Date: 2010-06-19T20:14:50+02:00
List-Id: <comp.lang.ada>

"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.