sem_util.adb (Extensions_Visible_Status): Modify the logic to account for non-SPARK code.

2014-11-20  Hristian Kirtchev  <kirtchev@adacore.com>

	* sem_util.adb (Extensions_Visible_Status): Modify the logic to account
	for non-SPARK code.
	(Object_Access_Level): In ASIS mode, recognize
	a selected component with an implicit dereference so that it
	yields the same value with and without expansion.

From-SVN: r217839
This commit is contained in:
Hristian Kirtchev 2014-11-20 11:21:41 +00:00 committed by Arnaud Charlet
parent 5fde9688e0
commit a18d0b1580
2 changed files with 68 additions and 56 deletions

View File

@ -1,3 +1,11 @@
2014-11-20 Hristian Kirtchev <kirtchev@adacore.com>
* sem_util.adb (Extensions_Visible_Status): Modify the logic to account
for non-SPARK code.
(Object_Access_Level): In ASIS mode, recognize
a selected component with an implicit dereference so that it
yields the same value with and without expansion.
2014-11-20 Ed Schonberg <schonberg@adacore.com>
* sem_prag.adb (Analyze_Pragma, case Implemented): In ASIS

View File

@ -5929,10 +5929,8 @@ package body Sem_Util is
Subp : Entity_Id;
begin
if SPARK_Mode = On then
-- When a formal parameter is subject to Extensions_Visible, the
-- pragma is stored in the contract of related subprogram.
-- When a formal parameter is subject to Extensions_Visible, the pragma
-- is stored in the contract of related subprogram.
if Is_Formal (Id) then
Subp := Scope (Id);
@ -5958,7 +5956,7 @@ package body Sem_Util is
if Present (Arg1) then
Expr := Get_Pragma_Arg (Arg1);
-- Guarg against cascading errors when the argument of pragma
-- Guard against cascading errors when the argument of pragma
-- Extensions_Visible is not a valid static Boolean expression.
if Error_Posted (Expr) then
@ -5977,20 +5975,16 @@ package body Sem_Util is
return Extensions_Visible_True;
end if;
-- Otherwise pragma Expresions_Visible is not inherited or directly
-- specified, its value defaults to "False".
-- Otherwise pragma Extensions_Visible is not inherited or directly
-- specified. In SPARK code, its value defaults to "False".
else
elsif SPARK_Mode = On then
return Extensions_Visible_False;
end if;
-- When SPARK_Mode is disabled, all semantic checks related to pragma
-- Extensions_Visible are disabled as well. Instead of saturating the
-- code with "if SPARK_Mode /= Off then" checks, the predicate returns
-- a default value.
-- In non-SPARK code, pragma Extensions_Visible defaults to "True"
else
return Extensions_Visible_None;
return Extensions_Visible_True;
end if;
end Extensions_Visible_Status;
@ -15364,10 +15358,20 @@ package body Sem_Util is
-- recursive call on the prefix, which will in turn check the level
-- of the prefix object of the selected discriminant.
-- In Ada 2012, if the discriminant has implicit dereference and
-- the context is a selected component, treat this as an object of
-- unknown scope (see below). This is necessary in compile-only mode;
-- otherwise expansion will already have transformed the prefix into
-- a temporary.
if Nkind (Prefix (Obj)) = N_Selected_Component
and then Ekind (Etype (Prefix (Obj))) = E_Anonymous_Access_Type
and then
Ekind (Entity (Selector_Name (Prefix (Obj)))) = E_Discriminant
and then
(not Has_Implicit_Dereference
(Entity (Selector_Name (Prefix (Obj))))
or else Nkind (Parent (Obj)) /= N_Selected_Component)
then
return Object_Access_Level (Prefix (Obj));