OpenE2K/gcc
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

[Ada] GNATprove: avoid crash on illegal borrow during package elaboration

Browse Source 
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
This commit is contained in:
Yannick Moy 2019-09-17 08:02:15 +00:00 committed by Pierre-Marie de Rodat
parent 86ae194fdb
commit 8df56dfc69
2 changed files with 13 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
gcc/ada/ChangeLog
View File

@ -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> 2019-09-17 Bob Duff <duff@adacore.com>
* doc/gnat_ugn/gnat_and_program_execution.rst: Clarify * doc/gnat_ugn/gnat_and_program_execution.rst: Clarify

12
gcc/ada/sem_spark.adb
View File

@ -1419,12 +1419,12 @@ package body Sem_SPARK is
Target : constant Entity_Id := Defining_Identifier (Decl); Target : constant Entity_Id := Defining_Identifier (Decl);
Target_Typ : constant Node_Id := Etype (Target); Target_Typ : constant Node_Id := Etype (Target);
Expr : Node_Id; Expr : Node_Id;
Dummy : Boolean := True; Legal : Boolean := True;
begin begin
-- Start with legality rules not related to permissions -- 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 -- Now check permission-related legality rules
@ -1432,7 +1432,7 @@ package body Sem_SPARK is
when N_Full_Type_Declaration => when N_Full_Type_Declaration =>
null; null;
-- ??? What about component declarations with defaults. -- ??? What about component declarations with defaults.
when N_Subtype_Declaration => when N_Subtype_Declaration =>
Check_Expression (Subtype_Indication (Decl), Read); Check_Expression (Subtype_Indication (Decl), Read);
@ -1440,11 +1440,15 @@ package body Sem_SPARK is
when N_Object_Declaration => when N_Object_Declaration =>
Expr := Expression (Decl); Expr := Expression (Decl);
if Present (Expr) then if Legal and then Present (Expr) then
Check_Assignment (Target => Target, Check_Assignment (Target => Target,
Expr => Expr); Expr => Expr);
end if; 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 if Is_Deep (Target_Typ) then
declare declare
Tree : constant Perm_Tree_Access := Tree : constant Perm_Tree_Access :=