* [Ada] GNATprove: avoid crash on illegal borrow during package elaboration
@ 2019-09-17 8:07 Pierre-Marie de Rodat
0 siblings, 0 replies; only message in thread
From: Pierre-Marie de Rodat @ 2019-09-17 8:07 UTC (permalink / raw)
To: gcc-patches; +Cc: Yannick Moy
[-- Attachment #1: Type: text/plain, Size: 442 bytes --]
In GNATprove, a borrow during package elaboration is illegal, but a
crash could be issued when analyzing the corresponding declaration. Now
avoid analyzing the declaration in that case.
There is no test as this does not impact compilation.
Tested on x86_64-pc-linux-gnu, committed on trunk
2019-09-17 Yannick Moy <moy@adacore.com>
gcc/ada/
* sem_spark.adb (Check_Declaration): Do not check the assignment
from an illegal declaration.
[-- Attachment #2: patch.diff --]
[-- Type: text/x-diff, Size: 1621 bytes --]
--- gcc/ada/sem_spark.adb
+++ gcc/ada/sem_spark.adb
@@ -1419,12 +1419,12 @@ package body Sem_SPARK is
Target : constant Entity_Id := Defining_Identifier (Decl);
Target_Typ : constant Node_Id := Etype (Target);
Expr : Node_Id;
- Dummy : Boolean := True;
+ Legal : Boolean := True;
begin
-- Start with legality rules not related to permissions
- Check_Declaration_Legality (Decl, Force => True, Legal => Dummy);
+ Check_Declaration_Legality (Decl, Force => True, Legal => Legal);
-- Now check permission-related legality rules
@@ -1432,7 +1432,7 @@ package body Sem_SPARK is
when N_Full_Type_Declaration =>
null;
- -- ??? What about component declarations with defaults.
+ -- ??? What about component declarations with defaults.
when N_Subtype_Declaration =>
Check_Expression (Subtype_Indication (Decl), Read);
@@ -1440,11 +1440,15 @@ package body Sem_SPARK is
when N_Object_Declaration =>
Expr := Expression (Decl);
- if Present (Expr) then
+ if Legal and then Present (Expr) then
Check_Assignment (Target => Target,
Expr => Expr);
end if;
+ -- Always add variable to the current permission environment,
+ -- even in the illegal case, as the rest of the analysis expects
+ -- to find it.
+
if Is_Deep (Target_Typ) then
declare
Tree : constant Perm_Tree_Access :=
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2019-09-17 8:07 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2019-09-17 8:07 [Ada] GNATprove: avoid crash on illegal borrow during package elaboration Pierre-Marie de Rodat
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).