Put_Image aspect and Spark

General
1

How to use the Put_Image aspect in Spark code?

I get the following error with gnatprove for the example specification below.

test-put_images.ads:10:06: error: "Root_Buffer_Type'Class" is not allowed in SPARK (due to primitive calls in default initial condition)
   10 |     Put_Image => Image;
      |     ^~~~~~~~~
  violation of aspect SPARK_Mode at line 5
    5 |package Test.Put_Images with Spark_Mode is
      |                             ^ here

test-put_images.ads:13:07: error: "Root_Buffer_Type'Class" is not allowed in SPARK (due to primitive calls in default initial condition)
   13 |     (Output : in out Ada.Strings.Text_Buffers.Root_Buffer_Type'Class;
      |      ^~~~~~
  violation of aspect SPARK_Mode at line 5
    5 |package Test.Put_Images with Spark_Mode is
      |                             ^ here

Spec:

pragma Ada_2022;

with Ada.Strings.Text_Buffers;

package Test.Put_Images with Spark_Mode is

   type T is record
      Value : Integer := 1;
   end record with
     Put_Image => Image;

   procedure Image
     (Output : in out Ada.Strings.Text_Buffers.Root_Buffer_Type'Class;
      Item   :        T);

end Test.Put_Images;
1 Like