FreeChainXenon/gcc
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

[Ada] Handle pragmas that come from aspects for GNATprove

Browse source 
In GNATprove we appear to abuse a routine related to cross-references and
expect it to deliver exact results, which is not what it was designed for.

This patch is a temporary solution to avoid crashes in GNATprove; it doesn't
affect the frontend or other backends, because this code is used exclusively
by GNATprove (it is located in the frontend for technical reasons). No tests
provided.

2018-08-21  Piotr Trojanek  <trojanek@adacore.com>

gcc/ada/

	* lib-xref.ads, lib-xref-spark_specific.adb
	(Enclosing_Subprogram_Or_Library_Package): Now roughtly works
	for pragmas that come from aspect specifications.

From-SVN: r263707
This commit is contained in:
Piotr Trojanek 2018-08-21 14:44:30 +00:00 • committed by Pierre-Marie de Rodat
parent d40800cfe5
commit b7e875ce96
3 changed files with 22 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
gcc/ada/ChangeLog
View file

@ -1,3 +1,9 @@
2018-08-21 Piotr Trojanek <trojanek@adacore.com>
* lib-xref.ads, lib-xref-spark_specific.adb
(Enclosing_Subprogram_Or_Library_Package): Now roughtly works
for pragmas that come from aspect specifications.
2018-08-21 Pierre-Marie de Rodat <derodat@adacore.com>
* sa_messages.ads, sa_messages.adb: New source files.

12
gcc/ada/lib-xref-spark_specific.adb
View file

@ -228,7 +228,17 @@ package body SPARK_Specific is
end loop;
if Nkind (Context) = N_Pragma then
Context := Parent (Context);
-- When used for cross-references then aspects might not be
-- yet linked to pragmas; when used for AST navigation in
-- GNATprove this routine is expected to follow those links.
if From_Aspect_Specification (Context) then
Context := Corresponding_Aspect (Context);
pragma Assert (Nkind (Context) = N_Aspect_Specification);
Context := Entity (Context);
else
Context := Parent (Context);
end if;
end if;
when N_Entry_Body

5
gcc/ada/lib-xref.ads
View file

@ -632,6 +632,11 @@ package Lib.Xref is
-- Return the closest enclosing subprogram or library-level package.
-- This ensures that GNATprove can distinguish local variables from
-- global variables.
--
-- ??? This routine should only be used for processing related to
-- cross-references, where it might return wrong result but must avoid
-- crashes on ill-formed source code. It is wrong to use it where exact
-- result is needed.
procedure Generate_Dereference
(N : Node_Id;