Spark: variable "not initialized" when it is (but full type declaration in private, non-spark part of the package)

General
1

Hi, my book is older than the introduction of access types in spark so maybe that’s why I missed something. So we have a case of a package whose public part is in Spark but not the private part nor the body. The driver is also spark. Goes like this:

private with Ada.Finalization;
package Interval_Trees with SPARK_Mode => On
is
   type Interval is record
         Low  : Float;
         High : Float;
      end record with Predicate => Low < High;
   type Tree is limited private;
   procedure Insert (T : in out Tree; Item : in Interval) with Depends => (T => (T, Item));
  function Check_Overlap (T : Tree; Item : Interval) return Boolean;
private
   pragma SPARK_Mode (Off);
   type Tree_Node;
   type Tree_Node_Access is access Tree_Node;
   type Tree_Node is record
      -- irrelevant
   end record;
   type Tree is new Ada.Finalization.Limited_Controlled with record
         Root  : Tree_Node_Access := null;
         Count : Natural := 0;
      end record;
   overriding procedure Finalize (T : in out Tree);
end Interval_Trees;

While the driver goes like this:

with Interval_Trees, gnat.IO; use Interval_Trees, gnat.IO;
procedure interval_test with spark_mode is
	T: Tree;
begin
	Insert (T, (19.33, 29.0));
	put_line (Check_overlap(T, (1.00, 24.2))'Image);
end interval_test;

Gnatprove complains that T is not initialized when Insert is called, and that memory might not be initialized when Check_overlap tries to read it. But T is default-initialized, and both subprograms takes the null value into account.
Maybe it comes from the full type and default value being out of reach for the prover ?

2

You are right it’s probably related to SPARK_Mode (Off). SPARK doesn’t see the type definition so can’t tell whether it’s initialized or not. Luckily you can annotate the private type with the Default_Initial_Condition property. See chapter 5 of the SPARK UG.

3

Aspect Default_Initial_Condition can also be specified without argument to only indicate that default initialized variables of that type are considered as fully initialized

Perfect, thank you !

4

This should work:

   type T is limited private with Default_Initial_Condition;
1 Like
5

First failing VC is discharged, but not the second about Check_Overlap. No difference with higher levels.

interval_test.adb:7:19: medium: “memory accessed through objects of access type” might not be initialized after elaboration of main program “interval_test”
7 | put_line (Check_overlap(T, (1.00, 24.2))'Image);