Tasking in SPARK requires sequential elaboration

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 get this weird error that I was not able to find a fix for 11:14 tasking in SPARK requires sequential elaboration (SPARK RM 9(2)) violation of pragma SPARK_Mode

The original code is a little long but I was able to get the same error with a minimal example.

The specification:

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;

The implementation:

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;

Any help is appreciated :-)

Solution

You need the extra configuration pragma

pragma Partition_Elaboration_Policy (Sequential);

(see ARM H.6). For the example you give, this only needs to be placed on the spec; but in general it needs to be a program-wide configuration pragma.

You arrange this by having a file, say gnat.adc, containing for example

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

and referencing it in package Builder in your GNAT project file:

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