From 42e2600a7aab688b6399d278ee552f3703fb3b3d Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Thu, 19 Jan 2017 12:39:55 +0100 Subject: [multiple changes] 2017-01-19 Steve Baird * sem_util.ads: Add new Use_Full_View Boolean parameter to Get_Index_Bounds. * sem_util.adb (Get_Index_Bounds): replace calls to Scalar_Range with calls to a newly-defined Scalar_Range_Of_Right_View function. 2017-01-19 Arnaud Charlet * gnat1drv.adb: minor fix of unbalanced parens in comment * lib-xref.ads (Traverse_Compilation_Unit): declaration moved to visible part of the package to allow re-use in GNATprove. * lib-xref-spark_specific.adb (Traverse_Stub): routine refactored from repeated code of Traverse_Compilation_Unit. (Traverse_Declaration_Or_Statement): fixed detection of generic subprograms and packages; also, iteration over case statement alternatives rewritten to avoid testing if the first alternative is present (since it must be present due to Ada syntax restrictions). From-SVN: r244617 --- gcc/ada/lib-xref-spark_specific.adb | 98 +++++++++++++++++++------------------ 1 file changed, 51 insertions(+), 47 deletions(-) (limited to 'gcc/ada/lib-xref-spark_specific.adb') diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb index b74489f..e7239ec 100644 --- a/gcc/ada/lib-xref-spark_specific.adb +++ b/gcc/ada/lib-xref-spark_specific.adb @@ -99,13 +99,6 @@ package body SPARK_Specific is function Entity_Hash (E : Entity_Id) return Entity_Hashed_Range; -- Hash function for hash table - 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 flag - -- Inside_Stubs is True, then the body of stubs is also traversed. Generic - -- declarations are ignored. - -------------------- -- Add_SPARK_File -- -------------------- @@ -1269,63 +1262,54 @@ package body SPARK_Specific is --------------------------------------- procedure Traverse_Declaration_Or_Statement (N : Node_Id) is + function Traverse_Stub (N : Node_Id) return Boolean; + -- Returns True iff stub N should be traversed + + function Traverse_Stub (N : Node_Id) return Boolean is + begin + pragma Assert (Nkind_In (N, N_Package_Body_Stub, + N_Protected_Body_Stub, + N_Subprogram_Body_Stub, + N_Task_Body_Stub)); + + return Inside_Stubs and then Present (Library_Unit (N)); + end Traverse_Stub; + + -- Start of processing for Traverse_Declaration_Or_Statement + begin case Nkind (N) is when N_Package_Declaration => Traverse_Visible_And_Private_Parts (Specification (N)); when N_Package_Body => - if Ekind (Defining_Entity (N)) /= E_Generic_Package then - Traverse_Package_Body (N); - end if; + Traverse_Package_Body (N); when N_Package_Body_Stub => - if Present (Library_Unit (N)) then - declare - Body_N : constant Node_Id := Get_Body_From_Stub (N); - begin - if Inside_Stubs - and then Ekind (Defining_Entity (Body_N)) /= - E_Generic_Package - then - Traverse_Package_Body (Body_N); - end if; - end; + if Traverse_Stub (N) then + Traverse_Package_Body (Get_Body_From_Stub (N)); end if; when N_Subprogram_Body => - if not Is_Generic_Subprogram (Defining_Entity (N)) then - Traverse_Subprogram_Body (N); - end if; + Traverse_Subprogram_Body (N); when N_Entry_Body => Traverse_Subprogram_Body (N); when N_Subprogram_Body_Stub => - if Present (Library_Unit (N)) then - declare - Body_N : constant Node_Id := Get_Body_From_Stub (N); - begin - if Inside_Stubs - and then - not Is_Generic_Subprogram (Defining_Entity (Body_N)) - then - Traverse_Subprogram_Body (Body_N); - end if; - end; + if Traverse_Stub (N) then + Traverse_Subprogram_Body (Get_Body_From_Stub (N)); end if; when N_Protected_Body => Traverse_Protected_Body (N); when N_Protected_Body_Stub => - if Present (Library_Unit (N)) and then Inside_Stubs then + if Traverse_Stub (N) then Traverse_Protected_Body (Get_Body_From_Stub (N)); end if; - when N_Protected_Type_Declaration - | N_Single_Protected_Declaration - => + when N_Protected_Type_Declaration => Traverse_Visible_And_Private_Parts (Protected_Definition (N)); when N_Task_Definition => @@ -1335,7 +1319,7 @@ package body SPARK_Specific is Traverse_Task_Body (N); when N_Task_Body_Stub => - if Present (Library_Unit (N)) and then Inside_Stubs then + if Traverse_Stub (N) then Traverse_Task_Body (Get_Body_From_Stub (N)); end if; @@ -1372,12 +1356,12 @@ package body SPARK_Specific is -- Process case branches declare - Alt : Node_Id; + Alt : Node_Id := First (Alternatives (N)); begin - Alt := First (Alternatives (N)); - while Present (Alt) loop + loop Traverse_Declarations_Or_Statements (Statements (Alt)); Next (Alt); + exit when No (Alt); end loop; end; @@ -1458,8 +1442,18 @@ package body SPARK_Specific is -- Traverse_Package_Body -- --------------------------- - procedure Traverse_Package_Body (N : Node_Id) renames - Traverse_Declarations_And_HSS; + procedure Traverse_Package_Body (N : Node_Id) is + Spec_E : constant Entity_Id := Unique_Defining_Entity (N); + begin + case Ekind (Spec_E) is + when E_Package => + Traverse_Declarations_And_HSS (N); + when E_Generic_Package => + null; + when others => + raise Program_Error; + end case; + end Traverse_Package_Body; ----------------------------- -- Traverse_Protected_Body -- @@ -1474,8 +1468,18 @@ package body SPARK_Specific is -- Traverse_Subprogram_Body -- ------------------------------ - procedure Traverse_Subprogram_Body (N : Node_Id) renames - Traverse_Declarations_And_HSS; + procedure Traverse_Subprogram_Body (N : Node_Id) is + Spec_E : constant Entity_Id := Unique_Defining_Entity (N); + begin + case Ekind (Spec_E) is + when E_Function | E_Procedure | Entry_Kind => + Traverse_Declarations_And_HSS (N); + when Generic_Subprogram_Kind => + null; + when others => + raise Program_Error; + end case; + end Traverse_Subprogram_Body; ------------------------ -- Traverse_Task_Body -- -- cgit v1.1