[Ada] Crash on ignored Ghost expression function

This patch updates freezing to ensure that freeze nodes are inserted
into the tree when the entity being frozen is non-Ghost, and the context
is an ignored Ghost spec expression.

2018-12-11  Hristian Kirtchev  <kirtchev@adacore.com>

gcc/ada/

	* exp_util.adb (Insert_Action): Add new formal parameter
	Spec_Expr_OK.
	(Insert_Actions): Add new formal parameter Spec_Expr_OK. Update
	all calls to Insert_Actions where relevant. Honour an insertion
	from a spec expression context when requested by the caller.
	* exp_util.ads (Insert_Action): Add new formal parameter
	Spec_Expr_OK.
	(Insert_Actions): Add new formal parameter Spec_Expr_OK.
	* freeze.adb (Add_To_Result): Force the insertion of the freeze
	node even when the context is a spec expression.

gcc/testsuite/

	* gnat.dg/ghost2.adb, gnat.dg/ghost2.ads: New testcase.

From-SVN: r266996
This commit is contained in:
Hristian Kirtchev 2018-12-11 11:10:42 +00:00 committed by Pierre-Marie de Rodat
parent 30a5fd0b46
commit e2819941fc
7 changed files with 110 additions and 28 deletions

View file

@ -1,3 +1,16 @@
2018-12-11 Hristian Kirtchev <kirtchev@adacore.com>
* exp_util.adb (Insert_Action): Add new formal parameter
Spec_Expr_OK.
(Insert_Actions): Add new formal parameter Spec_Expr_OK. Update
all calls to Insert_Actions where relevant. Honour an insertion
from a spec expression context when requested by the caller.
* exp_util.ads (Insert_Action): Add new formal parameter
Spec_Expr_OK.
(Insert_Actions): Add new formal parameter Spec_Expr_OK.
* freeze.adb (Add_To_Result): Force the insertion of the freeze
node even when the context is a spec expression.
2018-12-11 Jerome Lambourg <lambourg@adacore.com>
* vxaddr2line.adb, vxlink-bind.adb, vxlink-bind.ads,

View file

@ -6702,20 +6702,34 @@ package body Exp_Util is
-- Insert_Action --
-------------------
procedure Insert_Action (Assoc_Node : Node_Id; Ins_Action : Node_Id) is
procedure Insert_Action
(Assoc_Node : Node_Id;
Ins_Action : Node_Id;
Spec_Expr_OK : Boolean := False)
is
begin
if Present (Ins_Action) then
Insert_Actions (Assoc_Node, New_List (Ins_Action));
Insert_Actions
(Assoc_Node => Assoc_Node,
Ins_Actions => New_List (Ins_Action),
Spec_Expr_OK => Spec_Expr_OK);
end if;
end Insert_Action;
-- Version with check(s) suppressed
procedure Insert_Action
(Assoc_Node : Node_Id; Ins_Action : Node_Id; Suppress : Check_Id)
(Assoc_Node : Node_Id;
Ins_Action : Node_Id;
Suppress : Check_Id;
Spec_Expr_OK : Boolean := False)
is
begin
Insert_Actions (Assoc_Node, New_List (Ins_Action), Suppress);
Insert_Actions
(Assoc_Node => Assoc_Node,
Ins_Actions => New_List (Ins_Action),
Suppress => Suppress,
Spec_Expr_OK => Spec_Expr_OK);
end Insert_Action;
-------------------------
@ -6734,7 +6748,11 @@ package body Exp_Util is
-- Insert_Actions --
--------------------
procedure Insert_Actions (Assoc_Node : Node_Id; Ins_Actions : List_Id) is
procedure Insert_Actions
(Assoc_Node : Node_Id;
Ins_Actions : List_Id;
Spec_Expr_OK : Boolean := False)
is
N : Node_Id;
P : Node_Id;
@ -6745,14 +6763,20 @@ package body Exp_Util is
return;
end if;
-- Insert the action when the context is "Handling of Default and Per-
-- Object Expressions" only when requested by the caller.
if Spec_Expr_OK then
null;
-- Ignore insert of actions from inside default expression (or other
-- similar "spec expression") in the special spec-expression analyze
-- mode. Any insertions at this point have no relevance, since we are
-- only doing the analyze to freeze the types of any static expressions.
-- See section "Handling of Default Expressions" in the spec of package
-- Sem for further details.
-- See section "Handling of Default and Per-Object Expressions" in the
-- spec of package Sem for further details.
if In_Spec_Expression then
elsif In_Spec_Expression then
return;
end if;
@ -7431,7 +7455,8 @@ package body Exp_Util is
procedure Insert_Actions
(Assoc_Node : Node_Id;
Ins_Actions : List_Id;
Suppress : Check_Id)
Suppress : Check_Id;
Spec_Expr_OK : Boolean := False)
is
begin
if Suppress = All_Checks then
@ -7439,7 +7464,7 @@ package body Exp_Util is
Sva : constant Suppress_Array := Scope_Suppress.Suppress;
begin
Scope_Suppress.Suppress := (others => True);
Insert_Actions (Assoc_Node, Ins_Actions);
Insert_Actions (Assoc_Node, Ins_Actions, Spec_Expr_OK);
Scope_Suppress.Suppress := Sva;
end;
@ -7448,7 +7473,7 @@ package body Exp_Util is
Svg : constant Boolean := Scope_Suppress.Suppress (Suppress);
begin
Scope_Suppress.Suppress (Suppress) := True;
Insert_Actions (Assoc_Node, Ins_Actions);
Insert_Actions (Assoc_Node, Ins_Actions, Spec_Expr_OK);
Scope_Suppress.Suppress (Suppress) := Svg;
end;
end if;

View file

@ -90,38 +90,53 @@ package Exp_Util is
procedure Insert_Action
(Assoc_Node : Node_Id;
Ins_Action : Node_Id);
Ins_Action : Node_Id;
Spec_Expr_OK : Boolean := False);
-- Insert the action Ins_Action at the appropriate point as described
-- above. The action is analyzed using the default checks after it is
-- inserted. Assoc_Node is the node with which the action is associated.
-- When flag Spec_Expr_OK is set, insertions triggered in the context of
-- spec expressions are honoured, even though they contradict "Handling
-- of Default and Per-Object Expressions".
procedure Insert_Action
(Assoc_Node : Node_Id;
Ins_Action : Node_Id;
Suppress : Check_Id);
Suppress : Check_Id;
Spec_Expr_OK : Boolean := False);
-- Insert the action Ins_Action at the appropriate point as described
-- above. The action is analyzed using the default checks as modified
-- by the given Suppress argument after it is inserted. Assoc_Node is
-- the node with which the action is associated.
procedure Insert_Actions
(Assoc_Node : Node_Id;
Ins_Actions : List_Id);
-- Insert the list of action Ins_Actions at the appropriate point as
-- described above. The actions are analyzed using the default checks
-- after they are inserted. Assoc_Node is the node with which the actions
-- are associated. Ins_Actions may be No_List, in which case the call has
-- no effect.
-- the node with which the action is associated. When flag Spec_Expr_OK
-- is set, insertions triggered in the context of spec expressions are
-- honoured, even though they contradict "Handling of Default and Per-
-- Object Expressions".
procedure Insert_Actions
(Assoc_Node : Node_Id;
Ins_Actions : List_Id;
Suppress : Check_Id);
Spec_Expr_OK : Boolean := False);
-- Insert the list of action Ins_Actions at the appropriate point as
-- described above. The actions are analyzed using the default checks
-- after they are inserted. Assoc_Node is the node with which the actions
-- are associated. Ins_Actions may be No_List, in which case the call has
-- no effect. When flag Spec_Expr_OK is set, insertions triggered in the
-- context of spec expressions are honoured, even though they contradict
-- "Handling of Default and Per-Object Expressions".
procedure Insert_Actions
(Assoc_Node : Node_Id;
Ins_Actions : List_Id;
Suppress : Check_Id;
Spec_Expr_OK : Boolean := False);
-- Insert the list of action Ins_Actions at the appropriate point as
-- described above. The actions are analyzed using the default checks
-- as modified by the given Suppress argument after they are inserted.
-- Assoc_Node is the node with which the actions are associated.
-- Assoc_Node is the node with which the actions are associated. List
-- Ins_Actions may be No_List, in which case the call has no effect.
-- When flag Spec_Expr_OK is set, insertions triggered in the context of
-- spec expressions are honoured, even though they contradict "Handling
-- of Default and Per-Object Expressions".
procedure Insert_Action_After
(Assoc_Node : Node_Id;

View file

@ -2245,13 +2245,19 @@ package body Freeze is
-- entity being frozen is living. Insert the freezing action prior
-- to the start of the enclosing ignored Ghost region. As a result
-- the freezeing action will be preserved when the ignored Ghost
-- context is eliminated.
-- context is eliminated. The insertion must take place even when
-- the context is a spec expression, otherwise "Handling of Default
-- and Per-Object Expressions" will suppress the insertion, and the
-- freeze node will be dropped on the floor.
if Saved_GM = Ignore
and then Ghost_Mode /= Ignore
and then Present (Ignored_Ghost_Region)
then
Insert_Action (Ignored_Ghost_Region, Fnod);
Insert_Action
(Assoc_Node => Ignored_Ghost_Region,
Ins_Action => Fnod,
Spec_Expr_OK => True);
-- Otherwise add the freezing action to the result list

View file

@ -1,3 +1,7 @@
2018-12-11 Hristian Kirtchev <kirtchev@adacore.com>
* gnat.dg/ghost2.adb, gnat.dg/ghost2.ads: New testcase.
2018-12-11 Eric Botcazou <ebotcazou@adacore.com>
* gnat.dg/atomic11.adb, gnat.dg/atomic11_pkg1.ads,

View file

@ -0,0 +1,5 @@
-- { dg-do compile }
package body Ghost2 is
procedure Set is null;
end Ghost2;

View file

@ -0,0 +1,14 @@
package Ghost2 is
type Val_Entry is (A, B, C, D);
function Transition_Valid (L : Val_Entry; R : Val_Entry) return Boolean
is ((L = B and R = C) or
(L = C and R = C) or
(L = C and R = D) or
(L = D and R = B))
with Ghost;
procedure Set;
type Val_Array is array (1 .. 5) of Val_Entry;
end Ghost2;