From e5ce97d294608b4918b3809bc461052b58de8993 Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Tue, 9 Jul 2019 07:53:26 +0000 Subject: [PATCH] [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 gcc/ada/ * sem_spark.adb (Get_Perm_Or_Tree): Issue an error when encountering unknown global variable. From-SVN: r273267 --- gcc/ada/ChangeLog | 5 +++++ gcc/ada/sem_spark.adb | 11 ++++++++++- 2 files changed, 15 insertions(+), 1 deletion(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 9f6b789b983..0fd03b728d9 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,8 @@ +2019-07-09 Yannick Moy + + * sem_spark.adb (Get_Perm_Or_Tree): Issue an error when + encountering unknown global variable. + 2019-07-09 Yannick Moy * sem_spark.adb (Check_Expression): Change signature to take an diff --git a/gcc/ada/sem_spark.adb b/gcc/ada/sem_spark.adb index 2b1991959ab..6f27d20452d 100644 --- a/gcc/ada/sem_spark.adb +++ b/gcc/ada/sem_spark.adb @@ -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; -- 2.30.2