This patch suppresses the processing of references to internal variables for SPARK. As a result, this eliminates an infinite loop triggered by walking the scope chain of an internal variable which plays the role of an elaboration flag.
------------ -- Source -- ------------ -- gnat.adc pragma SPARK_Mode (On); -- pack1.ads package Pack1 is procedure Proc; end Pack1; -- pack1.adb package body Pack1 is procedure Proc is begin null; end Proc; end Pack1; -- pack2.ads package Pack2 is procedure Proc; end Pack2; -- pack2.adb with Pack1; package body Pack2 is procedure Proc is procedure Nested_Proc is begin Pack1.Proc; end Nested_Proc; begin Nested_Proc; end Proc; end Pack2; -- main.adb with Pack2; procedure Main is begin null; end Main; ----------------- -- Compilation -- ----------------- $ gnatmake -q -gnatE main.adb Tested on x86_64-pc-linux-gnu, committed on trunk 2017-09-08 Hristian Kirtchev <kirtc...@adacore.com> * sem_elab.adb (Check_A_Call): Do not consider references to internal variables for SPARK semantics.
Index: sem_elab.adb =================================================================== --- sem_elab.adb (revision 251863) +++ sem_elab.adb (working copy) @@ -721,23 +721,26 @@ and then not Is_Call_Of_Generic_Formal (N) then return; - end if; -- If this is a rewrite of a Valid_Scalars attribute, then nothing to -- check, we don't mind in this case if the call occurs before the body -- since this is all generated code. - if Nkind (Original_Node (N)) = N_Attribute_Reference + elsif Nkind (Original_Node (N)) = N_Attribute_Reference and then Attribute_Name (Original_Node (N)) = Name_Valid_Scalars then return; - end if; -- Intrinsics such as instances of Unchecked_Deallocation do not have -- any body, so elaboration checking is not needed, and would be wrong. - if Is_Intrinsic_Subprogram (E) then + elsif Is_Intrinsic_Subprogram (E) then return; + + -- Do not consider references to internal variables for SPARK semantics + + elsif Variable_Case and then not Comes_From_Source (E) then + return; end if; -- Proceed with check