SPARK gnatprove on Get_Line says "initialization check might fail"

General
1

I tried using Get_Line to read lines from a file back on Day 3 of Advent of Code and gnatprove gave me this result:

day3.adb:129:28: medium: initialization check might fail
  129 |      Get_Line (Data_File, Line, Last);
      |                           ^~~~
  in value of subprogram parameter after the call at day3.adb:129

I had initialized the entire line array to ‘0’ at the beginning of the program, and I couldn’t even figure out what it was complaining about, so I ended up replacing Get_Line with an equivalent loop. But now that I’m done with AoC I thought I’d ask if anyone has any insights about this. I did also check the value of Last to make sure it was in Line’Range before I tried to do anything with it.

Line is declared as:

Line : String (1 .. 1000);

Here’s the snippet of code around that line:

   Line := (others => '0');

   Open (File => Data_File,
         Mode => In_File,
         Name => "data/day3.txt");

   while not End_Of_File (Data_File) loop
      Get_Line (Data_File, Line, Last);
      if Last in Line'Range then

This was with gnatprove version 15.1.0.

2

The contract on that Get_Line procedure uses Relaxed_Initialization on the output string argument. So the variable you pass in for that argument (Line in this case) also needs to be declared with Relaxed_Initialization:

Line : String (1 .. 1000) with Relaxed_Initialization;
2 Likes
3

That worked, thank you!