diff options
| author | Arnaud Charlet <charlet@adacore.com> | 2016-05-02 09:48:55 +0000 |
|---|---|---|
| committer | Arnaud Charlet <charlet@gcc.gnu.org> | 2016-05-02 11:48:55 +0200 |
| commit | eff69022b3937d69e567c2ce397af7a601d3c64b (patch) | |
| tree | 3474893145e478a497050044fb0627daafc3ce65 | |
| parent | fb8d37efa6cb29cc7a2407b1d273d7a9cbf070e0 (diff) | |
| download | gcc-eff69022b3937d69e567c2ce397af7a601d3c64b.zip gcc-eff69022b3937d69e567c2ce397af7a601d3c64b.tar.gz gcc-eff69022b3937d69e567c2ce397af7a601d3c64b.tar.bz2 | |
lib-xref-spark_specific.adb (Add_SPARK_Scope): add task type scope.
2016-05-02 Arnaud Charlet <charlet@adacore.com>
* 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
| -rw-r--r-- | gcc/ada/ChangeLog | 8 | ||||
| -rw-r--r-- | gcc/ada/lib-xref-spark_specific.adb | 14 | ||||
| -rw-r--r-- | gcc/ada/spark_xrefs.ads | 4 |
3 files changed, 22 insertions, 4 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 9062859..10d30a4 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,5 +1,13 @@ 2016-05-02 Arnaud Charlet <charlet@adacore.com> + * 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 <charlet@adacore.com> + * make.adb: Minor: avoid an exception when calling gnatmake with no argument and gnatmake is built with checks on. * lib-xref-spark_specific.adb: Minor code cleanup. diff --git a/gcc/ada/lib-xref-spark_specific.adb b/gcc/ada/lib-xref-spark_specific.adb index e575150..d0321db 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 f02234f..f3bf1a3 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. |