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）。对于您给出的示例，这只需要放在规范上；但一般来说它需要是程序范围的配置编译指示。

您可以通过一个文件来安排它，例如gnat.adc，包含

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

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

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