From eff69022b3937d69e567c2ce397af7a601d3c64b Mon Sep 17 00:00:00 2001 From: Arnaud Charlet Date: Mon, 2 May 2016 09:48:55 +0000 Subject: [PATCH] lib-xref-spark_specific.adb (Add_SPARK_Scope): add task type scope. 2016-05-02 Arnaud Charlet * lib-xref-spark_specific.adb (Add_SPARK_Scope): add task type scope. (Detect_And_Add_SPARK_Scope): detect and add task type scope. (Enclosing_Subprogram_Or_Package): Respect boundaries of task and entry declarations. * spark_xrefs.ads: minor typo in comment. From-SVN: r235726 --- gcc/ada/ChangeLog | 8 ++++++++ gcc/ada/lib-xref-spark_specific.adb | 14 ++++++++++++-- gcc/ada/spark_xrefs.ads | 4 ++-- 3 files changed, 22 insertions(+), 4 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 90628591ebf..10d30a44731 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,11 @@ +2016-05-02 Arnaud Charlet + + * lib-xref-spark_specific.adb (Add_SPARK_Scope): add task type scope. + (Detect_And_Add_SPARK_Scope): detect and add task type scope. + (Enclosing_Subprogram_Or_Package): Respect boundaries of task + and entry declarations. + * spark_xrefs.ads: minor typo in comment. + 2016-05-02 Arnaud Charlet * make.adb: Minor: avoid an exception when calling gnatmake with diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb index e575150d2b5..d0321dbfa0d 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_Task_Type => Typ := Xref_Entity_Letters (Ekind (E)); @@ -382,7 +383,7 @@ package body SPARK_Specific is Key => Entity_Id, Hash => Entity_Hash, Equal => "="); - -- Package used to build a correspondance between entities and scope + -- Package used to build a correspondence between entities and scope -- numbers used in SPARK cross references. Nrefs : Nat := Xrefs.Last; @@ -1033,7 +1034,8 @@ package body SPARK_Specific is N_Subprogram_Declaration) or else Nkind_In (N, N_Task_Body, -- tasks - N_Task_Body_Stub) + N_Task_Body_Stub, + N_Task_Type_Declaration) then Add_SPARK_Scope (N); end if; @@ -1125,10 +1127,18 @@ package body SPARK_Specific is 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); + exit; + when others => Result := Parent (Result); end case; diff --git a/gcc/ada/spark_xrefs.ads b/gcc/ada/spark_xrefs.ads index f02234f9d14..f3bf1a38f76 100644 --- a/gcc/ada/spark_xrefs.ads +++ b/gcc/ada/spark_xrefs.ads @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 2011-2015, Free Software Foundation, Inc. -- +-- Copyright (C) 2011-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- -- @@ -133,7 +133,7 @@ package SPARK_Xrefs is -- FX dependency-number filename . entity-number entity - -- dependency-number and filename identity a file in FD lines + -- 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. -- 2.30.2