diff mbox series

[Ada] Continue decontruction of SPARK frontend cross-references

Message ID 20171108161636.GA23762@adacore.com
State New
Headers show
Series [Ada] Continue decontruction of SPARK frontend cross-references | expand

Commit Message

Pierre-Marie de Rodat Nov. 8, 2017, 4:16 p.m. UTC 
While traversing the AST to collect SPARK cross-references (which are used
to synthesize Global contracts for code with SPARK_Mode => Off), we always
traverse body stubs. There is no need to configure this by a parameter.

The modified code is only executed as part of GNATprove. Behaviour unchanged,
so no test provided.

Tested on x86_64-pc-linux-gnu, committed on trunk

2017-11-08  Piotr Trojanek  <trojanek@adacore.com>

	* lib-xref.ads, lib-xref-spark_specific.adb (Traverse_Declarations):
	Remove Inside_Stubs parameter.
diff mbox series

Patch

Index: lib-xref-spark_specific.adb
===================================================================
--- lib-xref-spark_specific.adb	(revision 254539)
+++ lib-xref-spark_specific.adb	(working copy)
@@ -230,14 +230,14 @@ 
          return;
       end if;
 
-      Traverse_Scopes (CU => Cunit (Uspec), Inside_Stubs => True);
+      Traverse_Scopes (CU => Cunit (Uspec));
 
       --  When two units are present for the same compilation unit, as it
       --  happens for library-level instantiations of generics, then add all
       --  scopes to the same SPARK file.
 
       if Ubody /= No_Unit then
-         Traverse_Scopes (CU => Cunit (Ubody), Inside_Stubs => True);
+         Traverse_Scopes (CU => Cunit (Ubody));
       end if;
 
       --  Make entry for new file in file table
@@ -1156,10 +1156,7 @@ 
    -- Traverse_Compilation_Unit --
    -------------------------------
 
-   procedure Traverse_Compilation_Unit
-     (CU           : Node_Id;
-      Inside_Stubs : Boolean)
-   is
+   procedure Traverse_Compilation_Unit (CU : Node_Id) is
       procedure Traverse_Block                      (N : Node_Id);
       procedure Traverse_Declaration_Or_Statement   (N : Node_Id);
       procedure Traverse_Declarations_And_HSS       (N : Node_Id);
@@ -1195,7 +1192,7 @@ 
                                         N_Subprogram_Body_Stub,
                                         N_Task_Body_Stub));
 
-            return Inside_Stubs and then Present (Library_Unit (N));
+            return Present (Library_Unit (N));
          end Traverse_Stub;
 
       --  Start of processing for Traverse_Declaration_Or_Statement
Index: lib-xref.ads
===================================================================
--- lib-xref.ads	(revision 254539)
+++ lib-xref.ads	(working copy)
@@ -647,12 +647,9 @@ 
 
       generic
          with procedure Process (N : Node_Id) is <>;
-      procedure Traverse_Compilation_Unit
-        (CU           : Node_Id;
-         Inside_Stubs : Boolean);
-      --  Call Process on all declarations within compilation unit CU. If
-      --  Inside_Stubs is True, then the body of stubs is also traversed.
-      --  Generic declarations are ignored.
+      procedure Traverse_Compilation_Unit (CU : Node_Id);
+      --  Call Process on all declarations within compilation unit CU. Bodies
+      --  of stubs are also traversed, but generic declarations are ignored.
 
    end SPARK_Specific;