Sorry, I have to bother you with a SPARK question again… I still lack the experience to understand all problem causes, especially the following one.
I have type Dimension is range 1 .. 140, an Input which is a two-dimensional array (Dimension'Range, Dimension'Range) of Character, and a function that takes a coordinate and checks the surroundings of that coordinate, making sure it stays within the dimension bounds. If the surroundings match, it increases a count by 1. Here is a part of it:
function Number_Of_Xmas_Around (Row : Dimension; Col : Dimension) return Natural is
Count : Natural := 0;
begin
-- Check to the left (unless it's too close to the left edge).
if Col >= Dimension'First + 3 then
if Input (Row, Col - 1) = 'M' and Input (Row, Col - 2) = 'A' and Input (Row, Col - 3) = 'S' then
Count := @ + 1;
end if;
end if;
-- Similarly, check to the right, up, and down.
-- Check diagonal to the left and up (unless it's too close to the edges).
if Row >= Dimension'First + 3 and Col >= Dimension'First + 3 then
if Input (Row - 1, Col - 1) = 'M' and Input (Row - 2, Col - 2) = 'A' and Input (Row - 3, Col - 3) = 'S' then
Count := @ + 1;
end if;
end if;
-- Similarly, check the other diagonals.
pragma Assert (Count >= 0);
pragma Assert (Count <= 8);
-- There can be at most 8 matches,
-- because we do 8 checks and for each increase by 1 if it's true.
return Count;
end Number_Of_Xmas_Around;
(Full code is here.)
When I run gnatprove, it seems to have a problem with the diagonal checks, but I don’t understand what exactly. It says:
overflow check might fail, cannot prove lower bound for @ + 1
I don’t think this is the real problem, because the lower bound is obviously 0. And it only complains about the last three increases. If I remove the last three diagonal checks, it’s fine - although it still cannot prove the assertions. If I remove all diagonal checks, also the assertions are fine.
Does anyone have a hint what might be the problem? 
