Ada SPARK中用Sequential_IO读二进制文件触发gnatprove错误的解决咨询

代码实现 #

utils-file.ads 文件 #

package Utils.File with
   SPARK_Mode
is
    procedure Read_Content (File_Name : String);
end Utils.File;

utils-file.adb 文件 #

with Interfaces;
with Ada.Sequential_IO;

package body Utils.File with
   SPARK_Mode => Off
is
    package Seq is new Ada.Sequential_IO (Interfaces.Unsigned_8);

    procedure Read_Content (File_Name : String) with
       SPARK_Mode => Off
    is
        Handle : Seq.File_Type;
        Item   : Interfaces.Unsigned_8 := 0;
    begin
        Seq.Open (Handle, Seq.In_File, File_Name);
        Seq.Read (Handle, Item);
        Seq.Close (Handle);
    end Read_Content;
end Utils.File;

主程序 Main.adb #

with Utils.File;

procedure Main with
   SPARK_Mode => On
is
begin
    Utils.File.Read_Content ("foo.bin");
end Main;

检测到的错误 #

运行gnatprove时出现以下中等严重级别的错误：

main.adb:7:15: medium: "memory accessed through objects of access type" might not be initialized after elaboration of main program "Main"

问题背景 #

使用Text_IO替代Sequential_IO时不会触发该错误，但需求是读取二进制文件，必须使用Sequential_IO。

错误原因 #

这个错误的本质是：Ada.Sequential_IO的内部实现使用了访问类型（指针），而SPARK模式下的静态分析无法穿透标记为SPARK_Mode => Off的代码块，去验证这些访问类型指向的内存在程序初始化阶段是否已正确初始化。即使代码中已经正确关闭了文件句柄，SPARK也只能看到主程序调用了一个非SPARK兼容的过程，因此抛出内存未初始化的警告。

解决方法 #

有两种可行的处理方式：

1. 针对性抑制警告 #

如果确认代码逻辑安全，可以在主程序中添加编译指示，屏蔽该特定警告：

with Utils.File;

procedure Main with
   SPARK_Mode => On
is
   pragma Warnings (Off, """memory accessed through objects of access type"" might not be initialized");
begin
   Utils.File.Read_Content ("foo.bin");
end Main;

2. 改用SPARK兼容的文件操作包 #

使用Ada.Streams.Stream_IO替代Sequential_IO，它的实现更符合SPARK的验证要求，同样支持二进制文件读取，且可以开启SPARK模式进行完整验证：

• 修改utils-file.ads（保持不变）：

  package Utils.File with
     SPARK_Mode
  is
     procedure Read_Content (File_Name : String);
  end Utils.File;
  

• 修改utils-file.adb：

  with Interfaces;
  with Ada.Streams.Stream_IO;
  
  package body Utils.File with
     SPARK_Mode => On
  is
     use Ada.Streams.Stream_IO;
     use Interfaces;
  
     procedure Read_Content (File_Name : String) is
        File : File_Type;
        Item : Unsigned_8 := 0;
     begin
        Open (File, In_File, File_Name);
        Read (File, Item'Write);
        Close (File);
     exception
        when others =>
           if Is_Open (File) then
              Close (File);
           end if;
           raise;
     end Read_Content;
  end Utils.File;
  

  这种方式下，GNATprove可以完整验证代码安全性，不会再抛出未初始化警告。

内容的提问来源于stack exchange，提问作者Rich