В SPARK не разрешен вызов изменчивой функции в конфликтующем контексте.

Question

В настоящее время я изучаю Аду во время университетского курса по языкам программирования в реальном времени и у меня есть вопрос о SPARK.

Я работаю над проектом с задачей, которая контролирует автономный источник питания. Эта задача имеет решающее значение для безопасности машины и поэтому должна быть максимально безошибочной, скажем, проверенной с помощью SPARK. Мне удалось запустить несколько вещей с другими вопросами по stackru, но я все еще сталкивался с ошибками, которые не смог исправить с помощью быстрого поиска в руководстве пользователя.

Ошибка call to a volatile function in interfering context is not allowed in SPARK со ссылкой на строку if monitoring_interface.is_all_config_set then ... в

task body monitoring_task is
      next_time : Time;
   begin
      --  Initialisation of next execution time
      next_time := Clock;
      --  Superloop
      loop
         Put_Line ("Run task monitoring");
         --  Load monitor configuration
         monitor_pfc_voltage.config := monitoring_interface.get_monitor_pfc_voltage_config;
         monitor_pfc_current.config := monitoring_interface.get_monitor_pfc_current_config;
         monitor_output_voltage.config := monitoring_interface.get_monitor_output_voltage_config;
         monitor_output_current.config := monitoring_interface.get_monitor_output_current_config;

         --  Check if module has been configured correctly
         --  Don't do anything otherwise
         if monitoring_interface.is_all_config_set then --  <= erroneous line
            do_monitoring;
         end if;

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

Функция is_all_config_set определяется в защищенном типе, который я использую для межзадачного общения.

package PSU_Monitoring is

   ... Declaration of some types (Monitor_Config_T) ...

   protected type Monitoring_Interface_T is
      function is_all_config_set return Boolean;

      procedure set_monitor_pfc_voltage_config (new_monitor_config : in Monitor_Config_T);
      function get_monitor_pfc_voltage_config return Monitor_Config_T;

      procedure set_monitor_pfc_current_config (new_monitor_config : in Monitor_Config_T);
      function get_monitor_pfc_current_config return Monitor_Config_T;

      procedure set_monitor_output_voltage_config (new_monitor_config : in Monitor_Config_T);
      function get_monitor_output_voltage_config return Monitor_Config_T;

      procedure set_monitor_output_current_config (new_monitor_config : in Monitor_Config_T);
      function get_monitor_output_current_config return Monitor_Config_T; 
   private
      --  Configuration for PFC intermediate voltage
      monitor_pfc_voltage_config : Monitor_Config_T;
      monitor_pfc_voltage_config_set : Boolean := False;
      --  Configuration for PFC inductor current
      monitor_pfc_current_config : Monitor_Config_T;
      monitor_pfc_current_config_set : Boolean := False;
      --  Configuration for output voltage
      monitor_output_voltage_config : Monitor_Config_T;
      monitor_output_voltage_config_set : Boolean := False;
      --  Configuration for output inductor current
      monitor_output_current_config : Monitor_Config_T;
      monitor_output_current_config_set : Boolean := False;
   end Monitoring_Interface_T;

   monitoring_interface : Monitoring_Interface_T;

private

... Declaration of a task and some private constants and subprograms ...

end PSU_Monitoring

Соответствующее тело

package body PSU_Monitoring is

   protected body Monitoring_Interface_T is

      function is_all_config_set return Boolean is
      begin
         return monitor_pfc_voltage_config_set and monitor_pfc_current_config_set and monitor_output_voltage_config_set and monitor_output_current_config_set;
      end is_all_config_set;

      procedure set_monitor_pfc_voltage_config (new_monitor_config : in Monitor_Config_T) is
      begin
         monitor_pfc_voltage_config := new_monitor_config;
         monitor_pfc_voltage_config_set := True;
      end set_monitor_pfc_voltage_config;

      function get_monitor_pfc_voltage_config return Monitor_Config_T is
      begin
         return monitor_pfc_voltage_config;
      end get_monitor_pfc_voltage_config;

      procedure set_monitor_pfc_current_config (new_monitor_config : in Monitor_Config_T) is
      begin
         monitor_pfc_current_config := new_monitor_config;
         monitor_pfc_current_config_set := True;
      end set_monitor_pfc_current_config;

      function get_monitor_pfc_current_config return Monitor_Config_T is
      begin
         return monitor_pfc_current_config;
      end get_monitor_pfc_current_config;

      procedure set_monitor_output_voltage_config (new_monitor_config : in Monitor_Config_T) is
      begin
         monitor_output_voltage_config := new_monitor_config;
         monitor_output_voltage_config_set := True;
      end set_monitor_output_voltage_config;

      function get_monitor_output_voltage_config return Monitor_Config_T is
      begin
         return monitor_output_voltage_config;
      end get_monitor_output_voltage_config;

      procedure set_monitor_output_current_config (new_monitor_config : in Monitor_Config_T) is
      begin
         monitor_output_current_config := new_monitor_config;
         monitor_output_current_config_set := True;
      end set_monitor_output_current_config;

      function get_monitor_output_current_config return Monitor_Config_T is
      begin
         return monitor_output_current_config;
      end get_monitor_output_current_config;

   end Monitoring_Interface_T;

... Definition of the remaining subprograms defined in the specification file ...

end PSU_Monitoring;

В чем здесь проблема?

Answer 1

Как говорил Джеффри, нам нужно увидеть ту часть программы, где отмечена ошибка. В общем, это связано с функциями с побочными эффектами, см. Справочное руководство: http://docs.adacore.com/spark2014-docs/html/lrm/packages.html

Такое же сообщение об ошибке может наблюдаться, если вы используете функцию Clock из пакета Real-Time "неправильным" способом:

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

procedure Main with SPARK_Mode is
    Last : Time := Clock;
begin

    -- some stuff happening here ...

    if Clock > Last + Milliseconds(100) then
        Put_Line("Too late");
    end if;
end Main;

Clock - это функция, которая имеет побочные эффекты (она возвращает разные значения каждый раз, когда вы ее вызываете), и в этом примере функция используется в так называемом "мешающем контексте" (определение см. В ссылке выше).

Решением было бы слегка переписать ваш код:

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

procedure Main with SPARK_Mode is
    Last : Time := Clock;
begin

    -- some code
    declare
        now : Time := Clock;
    begin      
        if now > Last + Milliseconds(100) then
            Put_Line("Too late");
        end if;
    end;
end Main;

Итак, в основном, вы делаете то, что изолируете вызовы функций с побочными эффектами в отдельном операторе, сохраняете результат в переменной, а затем используете переменную, в которой у вас был вызов ранее. Этот трюк должен помочь и с вашим вызовом защищенного объекта.