This is the mail archive of the
mailing list for the GCC project.
[Ada] Handle pragmas that come from aspects for GNATprove
- From: Pierre-Marie de Rodat <derodat at adacore dot com>
- To: gcc-patches at gcc dot gnu dot org
- Cc: Piotr Trojanek <trojanek at adacore dot com>
- Date: Tue, 21 Aug 2018 11:02:32 -0400
- Subject: [Ada] Handle pragmas that come from aspects for GNATprove
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
Tested on x86_64-pc-linux-gnu, committed on trunk
2018-08-21 Piotr Trojanek <email@example.com>
* lib-xref.ads, lib-xref-spark_specific.adb
(Enclosing_Subprogram_Or_Library_Package): Now roughtly works
for pragmas that come from aspect specifications.
@@ -228,7 +228,17 @@ package body SPARK_Specific is
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);
+ Context := Parent (Context);
+ end if;
@@ -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.
(N : Node_Id;