I'm currently learning Ada during a university course on real-time programming languages and have a question about SPARK.
I'm working on a project with a task that monitors an off-grid power supply. This task is crucial for machine safety and should therefore be as error free as possible, say proven with SPARK. I was able to get a few things running with other questions on stackoverflow but I still run into errors that I was not able to fix with quick searches in the user guide.
The error is call to a volatile function in interfering context is not allowed in SPARK with reference to the line if monitoring_interface.is_all_config_set then ... in
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;
The function is_all_config_set is defined within a protected type that I use for inter task communication.
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
The respective body is
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;
What is the problem here?
As Jeffrey was saying, we need to see the part of the program where the error is flagged. In general, this is related to functions with side effects, see reference manual: http://docs.adacore.com/spark2014-docs/html/lrm/packages.html#external-state-variables
The same error message can be observed if you use the Clock function from the Real-Time package in the "wrong" way:
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 is a function that has side effects (it returns different values every time you call it), and in this example the function is used in what's called an "interfering context" (see link above for a definition).
The solution would be to rewrite your code slightly:
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;
So, basically, what you do is isolate calls to functions with side effects into a separate statement, saving the result in a variable, and then use the variable where you had your call before. This trick should help with your call to the protected object, as well.