Re: Constraint_Error from arithmetic operations

[Phil Thornley <phil.jpthornley@gmail.com>]

In article <87wqw3pr8e.fsf@mid.deneb.enyo.de>, fw@deneb.enyo.de says...

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

An imported modular value will be assumed to be in range, but because 
the data are array elements, the hypothesis will be a quantified formula 
- something like:

H1:    for_all(i___1 : integer, 0 <= i___1 and i___1 <= 65535 -> 0 <= 
          element(data, [i___1]) and element(data, [i___1]) <= 255) .

The Simplifier will only be able to use this to prove
     element(data, [offset + 1]) >= 0
if it can first prove that offset + 1 is in [0, 65535].  Perhaps this is 
the problem.

Depending on the complexity of the code, it is possible that the 
conclusion is provable, but not proved by the Simplifier. (If you have 
Victor and Alt-Ergo included in the distribution then you can try using 
them to deal with provable VCs that the Simplifier doesn't prove.)

If you post SPARKable code then we can give more precise answers.

Cheers,

Phil