diff mbox series

[Ada] Infinite loop on call to nested subprogram with -gnatE in SPARK

Message ID 20170908100833.GA138716@adacore.com
State New
Headers show
Series [Ada] Infinite loop on call to nested subprogram with -gnatE in SPARK | expand

Commit Message

Arnaud Charlet Sept. 8, 2017, 10:08 a.m. UTC
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.
diff mbox series

Patch

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