OpenE2K/gcc
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

2016-05-02 Arnaud Charlet <charlet@adacore.com>

Browse Source 
* 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
This commit is contained in:
Arnaud Charlet 2016-05-02 10:00:00 +00:00 committed by Arnaud Charlet
parent 8d4611f7b0
commit 4871a41df9
4 changed files with 79 additions and 77 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
gcc/ada/ChangeLog
View File

@ -1,3 +1,17 @@
2016-05-02 Arnaud Charlet <charlet@adacore.com>
* 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 <kirtchev@adacore.com>
* lib-xref.ads, lib-xref-spark_specific.adb, get_spark_xrefs.adb,

111
gcc/ada/lib-xref-spark_specific.adb
View File

@ -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;
-----------------

6
gcc/ada/sem_intr.adb
View File

@ -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,

25
gcc/ada/spark_xrefs.ads
View File

@ -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")