This patch ensures that the Elaborate[_All] requirement imposed on the context of a unit in SPARK code is verified only when the static model is in effect.
------------ -- Source -- ------------ -- server.ads package Server with SPARK_Mode is function Read return Integer; end Server; -- server.adb package body Server with SPARK_Mode is function Read return Integer is begin return 0; end Read; end Server; -- client.ads package Client with SPARK_Mode is function Prf return Boolean; end Client; -- client.adb with Server; package body Client with SPARK_Mode is function Prf return Boolean is begin return Server.Read = 0; end Prf; end Client; ----------------- -- Compilation -- ----------------- $ gcc -c client.adb $ gcc -c client.adb -gnatE Tested on x86_64-pc-linux-gnu, committed on trunk 2017-10-09 Hristian Kirtchev <kirtc...@adacore.com> * sem_elab.adb (Static_Elaboration_Checks): Elaboration requirements are verified only in the static model.
Index: sem_elab.adb =================================================================== --- sem_elab.adb (revision 253564) +++ sem_elab.adb (working copy) @@ -5516,12 +5516,18 @@ Req_Met := False; + -- Elaboration requirements are verified only when the static model is + -- in effect because this diagnostic is graph-dependent. + + if not Static_Elaboration_Checks then + return; + -- If the target is within the main unit, either at the source level or -- through an instantiation, then there is no real requirement to meet -- because the main unit cannot force its own elaboration by means of an -- Elaborate[_All] pragma. Treat this case as valid coverage. - if In_Extended_Main_Code_Unit (Target_Id) then + elsif In_Extended_Main_Code_Unit (Target_Id) then Req_Met := True; -- Otherwise the target resides in an external unit