===================================================================
@@ -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
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 <kirtchev@adacore.com> * sem_elab.adb (Check_A_Call): Do not consider references to internal variables for SPARK semantics.