From 363f2c587eb0ae1238fe398326223ebc79c39cd3 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Mon, 26 Oct 2015 12:32:36 +0100 Subject: [PATCH] [multiple changes] 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. From-SVN: r229338 --- gcc/ada/ChangeLog | 14 +++++++ gcc/ada/lib-xref-spark_specific.adb | 59 +++++++++++------------------ gcc/ada/sem_prag.adb | 7 +++- 3 files changed, 42 insertions(+), 38 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index f2deda17c4e..61abaee34f9 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,17 @@ +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. + 2015-10-26 Yannick Moy * lib-xref-spark_specific.adb (Add_SPARK_Xrefs): Use character 'r' to 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 -- ----------------------------- diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index defb21a8858..779e91e0d16 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -14058,9 +14058,14 @@ package body Sem_Prag is Subp_Decl := Find_Related_Declaration_Or_Body (N, Do_Checks => True); + -- Abstract subprogram declaration + + if Nkind (Subp_Decl) = N_Abstract_Subprogram_Declaration then + null; + -- Generic subprogram declaration - if Nkind (Subp_Decl) = N_Generic_Subprogram_Declaration then + elsif Nkind (Subp_Decl) = N_Generic_Subprogram_Declaration then null; -- Body acts as spec -- 2.30.2