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 <troja...@adacore.com> * lib-xref.ads, lib-xref-spark_specific.adb (Traverse_Declarations): Remove Inside_Stubs parameter.
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;