Commit 38c2f655 by Maroua Maalej Committed by Pierre-Marie de Rodat

[Ada] SPARK: fix bug related to non access object permissions

2018-10-09  Maroua Maalej  <maalej@adacore.com>

gcc/ada/

	* sem_spark.adb (Check_Declaration): fix bug related to non
	access object permissions.

From-SVN: r264979
parent 827845b8
2018-10-09 Maroua Maalej <maalej@adacore.com>
* sem_spark.adb (Check_Declaration): fix bug related to non
access object permissions.
2018-10-09 Doug Rupp <rupp@adacore.com> 2018-10-09 Doug Rupp <rupp@adacore.com>
* libgnat/a-ncelfu.ads: Fix name in header to match package. * libgnat/a-ncelfu.ads: Fix name in header to match package.
......
...@@ -1052,22 +1052,6 @@ package body Sem_SPARK is ...@@ -1052,22 +1052,6 @@ package body Sem_SPARK is
end if; end if;
end if; end if;
elsif Nkind_In (Expression (Decl),
N_Attribute_Reference,
N_Attribute_Reference,
N_Expanded_Name,
N_Explicit_Dereference,
N_Indexed_Component,
N_Reference,
N_Selected_Component,
N_Slice)
then
if Is_Access_Type (Etype (Prefix (Expression (Decl))))
or else Is_Deep (Etype (Prefix (Expression (Decl))))
then
Current_Checking_Mode := Observe;
Check := True;
end if;
end if; end if;
end if; end if;
...@@ -1075,7 +1059,7 @@ package body Sem_SPARK is ...@@ -1075,7 +1059,7 @@ package body Sem_SPARK is
Check_Node (Expression (Decl)); Check_Node (Expression (Decl));
end if; end if;
-- If lhs is not a pointer, we still give it the appropriate -- If lhs is not a pointer, we still give it the unrestricted
-- state which is useless but not harmful. -- state which is useless but not harmful.
declare declare
...@@ -1215,7 +1199,7 @@ package body Sem_SPARK is ...@@ -1215,7 +1199,7 @@ package body Sem_SPARK is
when N_Attribute_Reference => when N_Attribute_Reference =>
case Attribute_Name (Expr) is case Attribute_Name (Expr) is
when Name_Access => when Name_Access =>
Error_Msg_N ("access attribute not allowed in SPARK", Expr); Error_Msg_N ("access attribute not allowed", Expr);
when Name_Last when Name_Last
| Name_First | Name_First
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment