Постановка задач в СПАРКе требует последовательной проработки

В настоящее время я изучаю Аду во время университетского курса по языкам программирования в реальном времени, и у меня есть вопрос о 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;

Любая помощь приветствуется :-)


ada gnat spark-ada
person Simon    schedule 21.01.2018    source источник

Ответы (1)


arrow_upward
4
arrow_downward

Вам нужна дополнительная прагма конфигурации

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";
   ...
person Simon Wright    schedule 21.01.2018
comment
Имеет ли установка политики разработки разделов на последовательную какие-либо прямые недостатки? Каковы другие возможные политики? - person Simon; 21.01.2018
comment
По крайней мере параллельно. Я дал ссылку выше на раздел 6 Приложения H ARM (Pragma Partition_Elaboration_Policy); тот же раздел в Annotated ARM находится здесь и немного подробнее. Это все, что я знаю! Есть некоторые изменения в поведении, но для правильных программ я сомневаюсь, что вы их заметите. Преимущество Sequential для программного обеспечения, которое должно быть надежным, заключается в том, что задачи не могут запускаться/прерываться, пока все не будет готово к работе (т. е. вы не получите никаких ошибок доступа до разработки). - person Simon Wright; 21.01.2018
comment
Похоже, что последовательный режим полностью подходит для моего приложения и, кроме того, необходим для SPARK. Я установил соответствующую прагму, и ошибки исчезли. Идеальный! - person Simon; 21.01.2018