Re: Constraint_Error from arithmetic operations

[Florian Weimer <fw@deneb.enyo.de>]

* 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?