From f6f401140a4a93899d25eeb05a537d35f4324f6f Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Tue, 27 Oct 2015 12:21:23 +0100 Subject: [PATCH] [multiple changes] 2015-10-27 Yannick Moy * lib-xref-spark_specific.adb (Enclosing_Subprogram_Or_Library_Package): detect library-level subprograms and handle entries as subprograms, i.e. now both library-level subprograms and entry bodies act as enclosing scopes. (Traverse_Declarations_Or_Statements): process entry bodies just like subprogram bodies. * lib-xref.ads (Enclosing_Subprogram_Or_Library_Package): comment simplified while keeping its the meaning and minor typo fixed ("of" -> "or"). * spark_xrefs.ads (Xref Section): fix in description of the ALI line for subprogram calls; such lines start with captial "F" followed by a space. 2015-10-27 Ed Schonberg * sem_ch8.adb (Find_Direct_Name): A parameter association is a legal context for applying an implicit dereference. (Analyze_Expanded_Name): Minor code cleanup. From-SVN: r229418 --- gcc/ada/ChangeLog | 22 ++++++++++++++++++++++ gcc/ada/lib-xref-spark_specific.adb | 12 ++++++++++++ gcc/ada/lib-xref.ads | 7 +++---- gcc/ada/sem_ch8.adb | 11 +++++++---- gcc/ada/spark_xrefs.ads | 2 +- 5 files changed, 45 insertions(+), 9 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 31765e92c5a..bb6af69ca50 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,25 @@ +2015-10-27 Yannick Moy + + * lib-xref-spark_specific.adb + (Enclosing_Subprogram_Or_Library_Package): detect library-level + subprograms and handle entries as subprograms, i.e. now both + library-level subprograms and entry bodies act as enclosing + scopes. + (Traverse_Declarations_Or_Statements): process entry bodies just + like subprogram bodies. + * lib-xref.ads (Enclosing_Subprogram_Or_Library_Package): comment + simplified while keeping its the meaning and minor typo fixed + ("of" -> "or"). + * spark_xrefs.ads (Xref Section): fix in description of the ALI + line for subprogram calls; such lines start with captial "F" + followed by a space. + +2015-10-27 Ed Schonberg + + * sem_ch8.adb (Find_Direct_Name): A parameter association is + a legal context for applying an implicit dereference. + (Analyze_Expanded_Name): Minor code cleanup. + 2015-10-27 Arnaud Charlet * sinput.ads, spark_xrefs.ads, lib-xref.adb: Fix typos. diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb index 631c87b1d81..fce0cf09d25 100644 --- a/gcc/ada/lib-xref-spark_specific.adb +++ b/gcc/ada/lib-xref-spark_specific.adb @@ -1032,6 +1032,12 @@ package body SPARK_Specific is and then Nkind (Parent (N)) in N_Subprogram_Specification then Result := Parent (Parent (Parent (N))); + + -- If this was a library-level subprogram then replace Result with + -- its Unit, which points to N_Subprogram_* node. + if Nkind (Result) = N_Compilation_Unit then + Result := Unit (Result); + end if; else Result := N; end if; @@ -1090,6 +1096,10 @@ package body SPARK_Specific is Result := Parent (Result); end if; + when N_Entry_Body => + Result := Defining_Identifier (Result); + exit; + when others => Result := Parent (Result); end case; @@ -1431,6 +1441,8 @@ package body SPARK_Specific is if Nkind (N) in N_Declaration or else Nkind (N) in N_Later_Decl_Item + or else + Nkind (N) = N_Entry_Body then Process (N); end if; diff --git a/gcc/ada/lib-xref.ads b/gcc/ada/lib-xref.ads index 9d1037ca053..63d78c7c169 100644 --- a/gcc/ada/lib-xref.ads +++ b/gcc/ada/lib-xref.ads @@ -624,10 +624,9 @@ package Lib.Xref is function Enclosing_Subprogram_Or_Library_Package (N : Node_Id) return Entity_Id; - -- Return the closest enclosing subprogram of package. Only return a - -- library level package. If the package is enclosed in a subprogram, - -- return the subprogram. This ensures that GNATprove can distinguish - -- local variables from global variables. + -- Return the closest enclosing subprogram or library-level package. + -- This ensures that GNATprove can distinguish local variables from + -- global variables. procedure Generate_Dereference (N : Node_Id; diff --git a/gcc/ada/sem_ch8.adb b/gcc/ada/sem_ch8.adb index bf39088d6e1..f02ec524340 100644 --- a/gcc/ada/sem_ch8.adb +++ b/gcc/ada/sem_ch8.adb @@ -597,8 +597,10 @@ package body Sem_Ch8 is begin -- If the entity pointer is already set, this is an internal node, or a -- node that is analyzed more than once, after a tree modification. In - -- such a case there is no resolution to perform, just set the type. For - -- completeness, analyze prefix as well. + -- such a case there is no resolution to perform, just set the type. + -- In either case, start by analyzing the prefix. + + Analyze (Prefix (N)); if Present (Entity (N)) then if Is_Type (Entity (N)) then @@ -607,7 +609,6 @@ package body Sem_Ch8 is Set_Etype (N, Etype (Entity (N))); end if; - Analyze (Prefix (N)); return; else Find_Expanded_Name (N); @@ -5615,12 +5616,14 @@ package body Sem_Ch8 is Set_Entity_Or_Discriminal (N, E); -- The name may designate a generalized reference, in which case - -- the dereference interpretation will be included. + -- the dereference interpretation will be included. Context is + -- one in which a name is legal. if Ada_Version >= Ada_2012 and then (Nkind (Parent (N)) in N_Subexpr or else Nkind_In (Parent (N), N_Object_Declaration, + N_Parameter_Association, N_Assignment_Statement)) then Check_Implicit_Dereference (N, Etype (E)); diff --git a/gcc/ada/spark_xrefs.ads b/gcc/ada/spark_xrefs.ads index 9201793b242..f6cc7c3de92 100644 --- a/gcc/ada/spark_xrefs.ads +++ b/gcc/ada/spark_xrefs.ads @@ -138,7 +138,7 @@ package SPARK_Xrefs is -- entity-number and identity identify a scope entity in FS lines for -- the file previously identified. - -- line typ col entity ref* + -- F line typ col entity ref* -- line is the line number of the referenced entity -- 2.30.2