Commit e5ce97d2 by Yannick Moy Committed by Pierre-Marie de Rodat

[Ada] Issue error on illegal ownership in SPARK

Check for declaration of global variables prior to use in the ownership
checking for SPARK.

There is no impact on compilation.

2019-07-09  Yannick Moy  <moy@adacore.com>

gcc/ada/

	* sem_spark.adb (Get_Perm_Or_Tree): Issue an error when
	encountering unknown global variable.

From-SVN: r273267
parent e0201d82
2019-07-09 Yannick Moy <moy@adacore.com>
* sem_spark.adb (Get_Perm_Or_Tree): Issue an error when
encountering unknown global variable.
2019-07-09 Yannick Moy <moy@adacore.com>
* sem_spark.adb (Check_Expression): Change signature to take an
Extended_Checking_Mode, for handling read permission checking of
sub-expressions in an assignment.
......
......@@ -3270,7 +3270,16 @@ package body Sem_SPARK is
C : constant Perm_Tree_Access :=
Get (Current_Perm_Env, Unique_Entity (Entity (N)));
begin
pragma Assert (C /= null);
-- Except during elaboration, the root object should have been
-- declared and entered into the current permission
-- environment.
if not Inside_Elaboration
and then C = null
then
Illegal_Global_Usage (N);
end if;
return (R => Unfolded, Tree_Access => C);
end;
......
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