Information Flo(w): Array Initialization in Loops
by Florian Schanda –
Dear diary,
Today I decided to look at a long standing SPARK annoyance. The flow analysis in SPARK will make sure all variables are initialized before use, but flow analysis in SPARK 2005 and 2014 are value independent. Record component accesses are static (you can write R.X, but X cannot be a variable), whereas array accesses can be dynamic (you can write A(X)). Flow analysis can distinguish between R.X and R.Y, but it cannot distinguish between A(2) and A(N). To see why this is important, consider the following code
procedure P (A : out Array_T) is
begin
for I in Index_T range 1 .. 27 loop
A (I) := Load_Data (I);
end loop;
end P;In previous versions of SPARK you would get a flow error stating that A might not be fully initialized, as in general it requires proof showing that all elements of A are assigned to and no references to not-yet-assigned elements are being made.
Although, in general this weakness remains, I have implemented an improvement for SPARK 2014 that recognises the obvious cases, so the code above will no longer produce flow errors (assuming it can be statically shown that 1 .. 27 covers the entire array). Of course, this also works for multi-dimensional arrays, so the following code will also be accepted without any false alarms
type Index_T is range 1 .. 10;
type M_Array_T is array (Index_T, Index_T) of Integer;
procedure Example (A : out M_Array_T) is
begin
for J in Index_T loop
for I in Index_T loop
if I < 5 then
A (I, J) := I + J;
else
A (I, J) := I - J;
end if;
end loop;
end loop;
end Example;