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: a07f3367d7,d144bcd39fd2a06b
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,ASCII-7-bit
X-Received: by 10.180.74.74 with SMTP id r10mr9875434wiv.3.1356837414507;
        Sat, 29 Dec 2012 19:16:54 -0800 (PST)
Path: 
 i11ni337233wiw.0!nntp.google.com!feeder3.cambriumusenet.nl!feed.tweaknews.nl!85.12.40.131.MISMATCH!xlned.com!feeder3.xlned.com!news.astraweb.com!border6.a.newsrouter.astraweb.com!border4.nntp.ams.giganews.com!border2.nntp.ams.giganews.com!border3.nntp.ams.giganews.com!border1.nntp.ams.giganews.com!nntp.giganews.com!newsreader4.netcologne.de!news.netcologne.de!feeder.erje.net!eu.feeder.erje.net!news.szaf.org!news.gnuher.de!news.enyo.de!.POSTED!not-for-mail
From: Florian Weimer <fw@deneb.enyo.de>
Newsgroups: comp.lang.ada
Subject: Re: Constraint_Error from arithmetic operations
Date: Thu, 27 Dec 2012 14:19:29 +0100
Message-ID: <87wqw3pr8e.fsf@mid.deneb.enyo.de>
References: <87r4mbrgl8.fsf@mid.deneb.enyo.de>
	<MPG.2b46340f43edd90398969f@news.zen.co.uk>
Mime-Version: 1.0
X-Trace: news.enyo.de 1356614368 31146 172.17.135.6 (27 Dec 2012 13:19:28 GMT)
X-Complaints-To: news@enyo.de
Cancel-Lock: sha1:Cty8jYJrG8j0e7ZTRvDUNtVvDTk=
Content-Type: text/plain; charset=us-ascii
Date: 2012-12-27T14:19:29+01:00
List-Id: <comp.lang.ada>

* Phil Thornley:

> (The publication dates of the three SPARK books are 1997, 2003, and 2012 
> so I'm not sure which one you mean).

My copy says (C) 2003, 2006, it doesn't say which edition.

> I don't know how you read the any of books to get that understanding, 
> but SPARK has always included the option to generate overflow checks 
> (and they are now always included whenever VCs are generated).

I see, thanks.  The book deals with this mainly in section 11.3
("Run-time checks"), which I had not come across yet.

> Originally the base range had to be specified using a 'base type 
> assertion' but the recent versions of the language have included the use 
> of derived types, as above.

Okay, The SPARK 2011 GPL edition in Debian wheezy does not seem to
support this yet.

Anyway, I got to the point where I've got useful .siv files, but I've
hit an obstacle: I've got an array

   type Byte is mod 256;
   type Data_Array_Index is range 0 .. 2**16 - 1;
   type Data_Array is array (Data_Array_Index) of Byte;

and Data is of type Data_Array_Index, but the Examiner cannot tell
that

    element(data, [offset + 1]) >= 0

This comes from an assignment

	    Content_Length := Data_Array_Index (Data (Offset + 1));

where Content_Length has type Data_Array_Index.

Should I just avoid modular types?