SPARK 中的任务需要按顺序细化

Question

我目前正在大学的实时编程语言课程中学习 Ada，并且有一个关于 SPARK 的问题。

我正在开展一个项目，其任务是监控离网电源。这项任务对机器安全至关重要，因此应尽可能避免错误，例如用 SPARK 证明。

我收到了这个奇怪的错误，我无法找到 11:14 tasking in SPARK requires sequential elaboration (SPARK RM 9(2)) violation of pragma SPARK_Mode 的修复方法

原始代码有点长，但我可以通过一个最小的示例得到相同的错误。

规格：

pragma Profile (Ravenscar);
pragma SPARK_Mode;

with System;

package simple_monitoring is

   function sign (val : in Float) return Float
     with Pre => val >= 10.0;

   task type myTask is
   end myTask;

end simple_monitoring;

实现：

pragma Profile (Ravenscar);
pragma SPARK_Mode;

with Ada.Real_Time; use Ada.Real_Time;
with Ada.Text_IO; use Ada.Text_IO;

package body simple_monitoring is

   function sign (val : in Float) return Float is
      res : Float;
   begin
      pragma Assert (val >= 10.0);
      res := 100.0 / val;

      return res;

   end sign;

   task body myTask is
      TASK_PERIOD : constant Time_Span := Milliseconds (100);
      next_time : Time := Clock;

      myVar : Float;
   begin
      loop
         Put_Line ("Running task");

         myVar := sign (20.0);

         next_time := next_time + TASK_PERIOD;
         delay until next_time;
      end loop;
   end myTask;

end simple_monitoring;

任何帮助表示赞赏:-)

Answer 1

你需要额外的配置编译指示

pragma Partition_Elaboration_Policy (Sequential);

（请参阅ARM H.6）。对于您给出的示例，只需将其放在规范中即可；但总的来说，它需要是程序范围的配置 pragma。

你可以通过一个文件来安排这个，比如gnat.adc，其中包含例如

pragma Profile (Ravenscar);
pragma Partition_Elaboration_Policy (Sequential);

并在您的 GNAT 项目文件中的包 Builder 中引用它：

package Builder is
   for Global_Configuration_Pragmas use "gnat.adc";
   ...