From 8df56dfc6991bda3c1cfa9d102c49d963763d5b4 Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Tue, 17 Sep 2019 08:02:15 +0000 Subject: [Ada] GNATprove: avoid crash on illegal borrow during package elaboration 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. 2019-09-17 Yannick Moy gcc/ada/ * sem_spark.adb (Check_Declaration): Do not check the assignment from an illegal declaration. From-SVN: r275788 --- gcc/ada/ChangeLog | 5 +++++ gcc/ada/sem_spark.adb | 12 ++++++++---- 2 files changed, 13 insertions(+), 4 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index f0d1f37..af3a2e7 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,8 @@ +2019-09-17 Yannick Moy + + * sem_spark.adb (Check_Declaration): Do not check the assignment + from an illegal declaration. + 2019-09-17 Bob Duff * doc/gnat_ugn/gnat_and_program_execution.rst: Clarify diff --git a/gcc/ada/sem_spark.adb b/gcc/ada/sem_spark.adb index af53f69..e4a8b3e 100644 --- a/gcc/ada/sem_spark.adb +++ b/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 := -- cgit v1.1