From 76890138f13c13ebc175f47f5d22eafd6a7975ca Mon Sep 17 00:00:00 2001 From: charlet Date: Mon, 26 Oct 2015 11:32:36 +0000 Subject: 2015-10-26 Yannick Moy * lib-xref-spark_specific.adb (Traverse_Protected_Declaration): New procedure for traversal. (Add_SPARK_Xrefs): Remove debugging code. (Traverse_Declaration_Or_Statement): Call the new traversal procedure. 2015-10-26 Hristian Kirtchev * sem_prag.adb (Analyze_Pragma): Pragma Extensions_Visible can now appear on an abstract subprogram declaration. git-svn-id: svn+ssh://gcc.gnu.org/svn/gcc/trunk@229338 138bc75d-0d04-0410-961f-82ee72b054a4 --- gcc/ada/lib-xref-spark_specific.adb | 59 ++++++++++++++----------------------- 1 file changed, 22 insertions(+), 37 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 a53942d59f9..631c87b1d81 100644 --- a/gcc/ada/lib-xref-spark_specific.adb +++ b/gcc/ada/lib-xref-spark_specific.adb @@ -124,10 +124,6 @@ package body SPARK_Specific is (N : Node_Id; Process : Node_Processing; Inside_Stubs : Boolean); - procedure Traverse_Package_Declaration - (N : Node_Id; - Process : Node_Processing; - Inside_Stubs : Boolean); procedure Traverse_Subprogram_Body (N : Node_Id; Process : Node_Processing; @@ -483,12 +479,7 @@ package body SPARK_Specific is begin for Index in SPARK_Scope_Table.First .. S - 1 loop if SPARK_Scope_Table.Table (Index).Scope_Entity = E then - declare - Dummy : constant SPARK_Scope_Record := - SPARK_Scope_Table.Table (Index); - begin - return True; - end; + return True; end if; end loop; @@ -523,13 +514,13 @@ package body SPARK_Specific is is begin -- The only references of interest on callable entities are calls. On - -- non-callable entities, the only references of interest are reads - -- and writes. + -- uncallable entities, the only references of interest are reads and + -- writes. if Ekind (E) in Overloadable_Kind then return Typ = 's'; - -- Objects of Task type or protected type are not SPARK references + -- Objects of task or protected types are not SPARK references elsif Present (Etype (E)) and then Ekind (Etype (E)) in Concurrent_Kind @@ -1254,7 +1245,14 @@ package body SPARK_Specific is begin case Nkind (N) is when N_Package_Declaration => - Traverse_Package_Declaration (N, Process, Inside_Stubs); + declare + Spec : constant Node_Id := Specification (N); + begin + Traverse_Declarations_Or_Statements + (Visible_Declarations (Spec), Process, Inside_Stubs); + Traverse_Declarations_Or_Statements + (Private_Declarations (Spec), Process, Inside_Stubs); + end; when N_Package_Body => if Ekind (Defining_Entity (N)) /= E_Generic_Package then @@ -1297,12 +1295,6 @@ package body SPARK_Specific is end; end if; - when N_Protected_Definition => - Traverse_Declarations_Or_Statements - (Visible_Declarations (N), Process, Inside_Stubs); - Traverse_Declarations_Or_Statements - (Private_Declarations (N), Process, Inside_Stubs); - when N_Protected_Body => Traverse_Protected_Body (N, Process, Inside_Stubs); @@ -1318,6 +1310,16 @@ package body SPARK_Specific is end; end if; + when N_Protected_Type_Declaration | N_Single_Protected_Declaration => + declare + Def : constant Node_Id := Protected_Definition (N); + begin + Traverse_Declarations_Or_Statements + (Visible_Declarations (Def), Process, Inside_Stubs); + Traverse_Declarations_Or_Statements + (Private_Declarations (Def), Process, Inside_Stubs); + end; + when N_Task_Definition => Traverse_Declarations_Or_Statements (Visible_Declarations (N), Process, Inside_Stubs); @@ -1481,23 +1483,6 @@ package body SPARK_Specific is (Handled_Statement_Sequence (N), Process, Inside_Stubs); end Traverse_Package_Body; - ---------------------------------- - -- Traverse_Package_Declaration -- - ---------------------------------- - - procedure Traverse_Package_Declaration - (N : Node_Id; - Process : Node_Processing; - Inside_Stubs : Boolean) - is - Spec : constant Node_Id := Specification (N); - begin - Traverse_Declarations_Or_Statements - (Visible_Declarations (Spec), Process, Inside_Stubs); - Traverse_Declarations_Or_Statements - (Private_Declarations (Spec), Process, Inside_Stubs); - end Traverse_Package_Declaration; - ----------------------------- -- Traverse_Protected_Body -- ----------------------------- -- cgit v1.2.1