1 files changed, 14 insertions, 0 deletions
diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb
index b8ea585..29f2f94 100644
--- a/gcc/ada/gnat1drv.adb
+++ b/gcc/ada/gnat1drv.adb
@@ -1045,6 +1045,20 @@ begin
       Original_Operating_Mode := Operating_Mode;
       Frontend;
 
+      --  In GNATprove mode, force loading of System unit when tasking is
+      --  used, so that in particular System.Interrupt_Priority is available
+      --  to GNATprove for the generation of VCs for checking the respect of
+      --  Ceiling Protocol.
+
+      if GNATprove_Mode and Opt.Tasking_Used then
+         declare
+            Unused_E : constant Entity_Id :=
+              Rtsfind.RTE (Rtsfind.RE_Interrupt_Priority);
+         begin
+            null;
+         end;
+      end if;
+
       --  Exit with errors if the main source could not be parsed
 
       if Sinput.Main_Source_File = No_Source_File then