指定另一个包中的子程序没有阻塞？

Question

SPARK 限制从受保护对象中调用可能阻塞的子程序。

但是，我注意到如果我在受保护对象所在的包之外调用任何子程序，我会收到有关可能阻塞子程序的警告。

我想用来告诉它调用将是非阻塞的外部包中缺少什么？我试过在另一个包中放一个“添加一个参数”子程序，但它不起作用。如果我将它移动到包含受保护对象的包中，它会这样做。

我错过了什么？

Answer 1

在 Ada 2020 中，有一个属性 Non_Blocking 明确标记静态分析的阻塞/非阻塞属性，编译器确保一切正确。

但是，如果您被困在 Ada 2012 中，这将无济于事 — 并且有些特定的东西会“潜在地阻塞”，例如入口调用和 [IIRC] 之类的东西，例如 Ada.Text_IO.Put — 而 SPARK 的推理是，如果它可能会阻塞，那么您无法确保它不是非阻塞的。

根据the RM，您需要注意以下几点：

在受保护的操作期间，调用 可能阻塞的操作。以下定义为 可能会阻塞操作：

• select_statement;
• accept_statement；
• entry_call_statement；
• delay_statement；
• 中止语句；
• 任务创建或激活；
• 对受保护子程序（或外部重新队列）的外部调用，其目标对象与受保护操作的目标对象相同；
• 对其主体包含潜在阻塞操作的子程序的调用。

因此，如果您尝试调用的子程序有 select、accept、delay 或 task，它可能会阻塞。

Answer 2

感谢@shark8 的详细回答。

我检查了我试图调用的方法的主体，因为它是一个简单的返回语句，它没有手册中提到的任何效果。

我确实但是发现在我尝试使用的包中打开SPARK_Mode => On 解决了这个问题。

这是重现该问题的 MwE：

-- main.adb

pragma Profile (GNAT_Extended_Ravenscar);
pragma Partition_Elaboration_Policy (Sequential);

with P1;

procedure Main is

begin
   --  Insert code here.
   null;
end Main;

-- simple.ads
package Simple is

   procedure Do_Nothing;

end Simple;

-- simple.adb 
package body Simple is

   procedure Do_Nothing is
   begin
      null;
   end Do_Nothing;


end Simple;

-- p1.ads
pragma Profile (GNAT_Extended_Ravenscar);
pragma Partition_Elaboration_Policy (Sequential);

package P1 with 
  SPARK_Mode => On 
is

   protected Protected_Object with 
     SPARK_Mode => On
   is
      procedure Do_Something;
   end Protected_Object;


end P1;

-- p1.adb 
with Simple;

package body P1 with 
  SPARK_Mode => On 
is

   protected body Protected_Object 
   with 
     SPARK_Mode => On 
   is      
      procedure Do_Something is 
      begin
         Simple.Do_Nothing;
      end Do_Something;
   end Protected_Object;


end P1;