From 4871a41df95577e9c43dcf118d46e7faf733ef94 Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Mon, 2 May 2016 10:00:00 +0000 Subject: [PATCH] 2016-05-02 Arnaud Charlet * spark_xrefs.ads Description of the spark cross-references clarified; small style fixes. * lib-xref-spark_specific.adb (Add_SPARK_Scope, Detect_And_Add_SPARK_Scope): consider protected types and bodies as yet another scopes. (Enclosing_Subprogram_Or_Library_Package): refactored using Hristian's suggestions; added support for scopes of protected types and bodies; fix for entries to return the scope of the enclosing concurrent type, which is consistent with what is returned for protected subprograms. * sem_intr.adb: Minor style fix in comment. From-SVN: r235731 --- gcc/ada/ChangeLog | 14 +++++ gcc/ada/lib-xref-spark_specific.adb | 111 ++++++++++++++++-------------------- gcc/ada/sem_intr.adb | 6 +- gcc/ada/spark_xrefs.ads | 25 ++++---- 4 files changed, 79 insertions(+), 77 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index ee9f265..eaab1b7 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,17 @@ +2016-05-02 Arnaud Charlet + + * spark_xrefs.ads Description of the spark cross-references + clarified; small style fixes. + * lib-xref-spark_specific.adb (Add_SPARK_Scope, + Detect_And_Add_SPARK_Scope): consider protected types and bodies + as yet another scopes. + (Enclosing_Subprogram_Or_Library_Package): refactored using + Hristian's suggestions; added support for scopes of protected + types and bodies; fix for entries to return the scope of the + enclosing concurrent type, which is consistent with what is + returned for protected subprograms. + * sem_intr.adb: Minor style fix in comment. + 2016-05-02 Hristian Kirtchev * lib-xref.ads, lib-xref-spark_specific.adb, get_spark_xrefs.adb, diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb index 10d1a05..46f7b3a 100644 --- a/gcc/ada/lib-xref-spark_specific.adb +++ b/gcc/ada/lib-xref-spark_specific.adb @@ -265,6 +265,7 @@ package body SPARK_Specific is | E_Generic_Package | E_Generic_Procedure | E_Package + | E_Protected_Type | E_Task_Type => Typ := Xref_Entity_Letters (Ekind (E)); @@ -284,7 +285,11 @@ package body SPARK_Specific is Typ := Xref_Entity_Letters (Ekind (E)); end if; - when E_Package_Body | E_Subprogram_Body | E_Task_Body => + when E_Package_Body + | E_Protected_Body + | E_Subprogram_Body + | E_Task_Body + => Typ := Xref_Entity_Letters (Ekind (Unique_Entity (E))); when E_Void => @@ -1029,6 +1034,10 @@ package body SPARK_Specific is N_Package_Body_Stub, N_Package_Declaration) or else + Nkind_In (N, N_Protected_Body, -- protected objects + N_Protected_Body_Stub, + N_Protected_Type_Declaration) + or else Nkind_In (N, N_Subprogram_Body, -- subprograms N_Subprogram_Body_Stub, N_Subprogram_Declaration) @@ -1048,63 +1057,44 @@ package body SPARK_Specific is function Enclosing_Subprogram_Or_Library_Package (N : Node_Id) return Entity_Id is - Result : Entity_Id; + Context : Entity_Id; begin -- If N is the defining identifier for a subprogram, then return the -- enclosing subprogram or package, not this subprogram. if Nkind_In (N, N_Defining_Identifier, N_Defining_Operator_Symbol) - and then Nkind (Parent (N)) in N_Subprogram_Specification + and then (Ekind (N) in Entry_Kind + or else Ekind (N) = E_Subprogram_Body + or else Ekind (N) in Generic_Subprogram_Kind + or else Ekind (N) in Subprogram_Kind) then - Result := Parent (Parent (Parent (N))); + Context := Parent (Unit_Declaration_Node (N)); - -- If this was a library-level subprogram then replace Result with + -- If this was a library-level subprogram then replace Context with -- its Unit, which points to N_Subprogram_* node. - if Nkind (Result) = N_Compilation_Unit then - Result := Unit (Result); + if Nkind (Context) = N_Compilation_Unit then + Context := Unit (Context); end if; else - Result := N; + Context := N; end if; - while Present (Result) loop - case Nkind (Result) is - when N_Package_Specification => + while Present (Context) loop + case Nkind (Context) is + when N_Package_Body | + N_Package_Specification => -- Only return a library-level package - if Is_Library_Level_Entity (Defining_Entity (Result)) then - Result := Defining_Entity (Result); + if Is_Library_Level_Entity (Defining_Entity (Context)) then + Context := Defining_Entity (Context); exit; else - Result := Parent (Result); + Context := Parent (Context); end if; - when N_Package_Body => - - -- Only return a library-level package - - if Is_Library_Level_Entity (Defining_Entity (Result)) then - Result := Defining_Entity (Result); - exit; - else - Result := Parent (Result); - end if; - - when N_Subprogram_Specification => - Result := Defining_Unit_Name (Result); - exit; - - when N_Subprogram_Declaration => - Result := Defining_Unit_Name (Specification (Result)); - exit; - - when N_Subprogram_Body => - Result := Defining_Unit_Name (Specification (Result)); - exit; - when N_Pragma => -- The enclosing subprogram for a precondition, postcondition, @@ -1112,51 +1102,46 @@ package body SPARK_Specific is -- pragma (skipping any other pragmas between this pragma and -- this declaration. - while Nkind (Result) = N_Pragma - and then Is_List_Member (Result) - and then Present (Prev (Result)) + while Nkind (Context) = N_Pragma + and then Is_List_Member (Context) + and then Present (Prev (Context)) loop - Result := Prev (Result); + Context := Prev (Context); end loop; - if Nkind (Result) = N_Pragma then - Result := Parent (Result); + if Nkind (Context) = N_Pragma then + Context := Parent (Context); end if; - when N_Entry_Body => - Result := Defining_Identifier (Result); - exit; - - when N_Entry_Declaration => - Result := Defining_Identifier (Result); - exit; - - when N_Task_Body => - Result := Defining_Identifier (Result); - exit; - - when N_Task_Type_Declaration => - Result := Defining_Identifier (Result); + when N_Entry_Body | + N_Entry_Declaration | + N_Protected_Type_Declaration | + N_Subprogram_Body | + N_Subprogram_Declaration | + N_Subprogram_Specification | + N_Task_Body | + N_Task_Type_Declaration => + Context := Defining_Entity (Context); exit; when others => - Result := Parent (Result); + Context := Parent (Context); end case; end loop; - if Nkind (Result) = N_Defining_Program_Unit_Name then - Result := Defining_Identifier (Result); + if Nkind (Context) = N_Defining_Program_Unit_Name then + Context := Defining_Identifier (Context); end if; -- Do not return a scope without a proper location - if Present (Result) - and then Sloc (Result) = No_Location + if Present (Context) + and then Sloc (Context) = No_Location then return Empty; end if; - return Result; + return Context; end Enclosing_Subprogram_Or_Library_Package; ----------------- diff --git a/gcc/ada/sem_intr.adb b/gcc/ada/sem_intr.adb index e25ebb7..a15e95c 100644 --- a/gcc/ada/sem_intr.adb +++ b/gcc/ada/sem_intr.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 1992-2015, Free Software Foundation, Inc. -- +-- Copyright (C) 1992-2016, Free Software Foundation, Inc. -- -- -- -- GNAT is free software; you can redistribute it and/or modify it under -- -- terms of the GNU General Public License as published by the Free Soft- -- @@ -59,7 +59,7 @@ package body Sem_Intr is procedure Check_Shift (E : Entity_Id; N : Node_Id); -- Check intrinsic shift subprogram, the two arguments are the same -- as for Check_Intrinsic_Subprogram (i.e. the entity of the subprogram - -- declaration, and the node for the pragma argument, used for messages) + -- declaration, and the node for the pragma argument, used for messages). procedure Errint (Msg : String; S : Node_Id; N : Node_Id); -- Post error message for bad intrinsic, the message itself is posted @@ -340,7 +340,7 @@ package body Sem_Intr is then null; - -- Exception functions + -- Exception functions elsif Nam_In (Nam, Name_Exception_Information, Name_Exception_Message, diff --git a/gcc/ada/spark_xrefs.ads b/gcc/ada/spark_xrefs.ads index f3bf1a3..fa958cf 100644 --- a/gcc/ada/spark_xrefs.ads +++ b/gcc/ada/spark_xrefs.ads @@ -36,7 +36,7 @@ package SPARK_Xrefs is -- SPARK cross-reference information can exist in one of two forms. In -- the ALI file, it is represented using a text format that is described - -- in this specification. Internally it is stored using three tables + -- in this specification. Internally it is stored using three tables: -- SPARK_Xref_Table, SPARK_Scope_Table and SPARK_File_Table, which are -- also defined in this unit. @@ -56,21 +56,21 @@ package SPARK_Xrefs is -- SPARK cross-reference information is generated on a unit-by-unit basis -- in the ALI file, using lines that start with the identifying character F - -- ("Formal"). These lines are generated if Frame_Condition_Mode is True. + -- ("Formal"). These lines are generated if GNATprove_Mode is True. -- The SPARK cross-reference information comes after the shared - -- cross-reference information, so it needs not be read by tools like - -- gnatbind, gnatmake etc. + -- cross-reference information, so it can be ignored by tools like + -- gnatbind, gnatmake, etc. -- ------------------- -- -- Scope Section -- -- ------------------- -- A first section defines the scopes in which entities are defined and - -- referenced. A scope is a package/subprogram declaration/body. Note that - -- a package declaration and body define two different scopes. Similarly, a - -- subprogram declaration and body, when both present, define two different - -- scopes. + -- referenced. A scope is a package/subprogram/protected_type/task_type + -- declaration/body. Note that a package declaration and body define two + -- different scopes. Similarly, a subprogram, protected type and task type + -- declaration and body, when both present, define two different scopes. -- FD dependency-number filename (-> unit-filename)? @@ -135,8 +135,11 @@ package SPARK_Xrefs is -- dependency-number and filename identify a file in FD lines - -- entity-number and identity identify a scope entity in FS lines for - -- the file previously identified. + -- entity-number and entity identify a scope in FS lines + -- for the file previously identified file. + + -- (filename and entity are just a textual representations of + -- dependency-number and entity-number) -- F line typ col entity ref* @@ -192,7 +195,7 @@ package SPARK_Xrefs is -- -- Generated Globals Section -- -- ------------------------------- - -- The Generated Globals section is located at the end of the ALI file. + -- The Generated Globals section is located at the end of the ALI file -- All lines introducing information related to the Generated Globals -- have the string "GG" appearing in the beginning. This string ("GG") -- 2.7.4