[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  <moy@adacore.com>

gcc/ada/

	* sem_spark.adb (Check_Declaration): Do not check the assignment
	from an illegal declaration.

From-SVN: r275788

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index f0d1f37dce7651000a6a300b9119c6082f939bd5..af3a2e7692de8f4793ac74f84db1209964902e9b 100644 (file)
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,8 @@
+2019-09-17  Yannick Moy  <moy@adacore.com>
+
+       * sem_spark.adb (Check_Declaration): Do not check the assignment
+       from an illegal declaration.
+
 2019-09-17  Bob Duff  <duff@adacore.com>
 
        * doc/gnat_ugn/gnat_and_program_execution.rst: Clarify

diff --git a/gcc/ada/sem_spark.adb b/gcc/ada/sem_spark.adb
index af53f69ba2c8fb2570cd2386abf0613b0818c388..e4a8b3ecaaf9e4eef9703e7591cf72b9f8632edf 100644 (file)
--- 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 :=