[Ada] Issue error on illegal ownership in SPARK

[Pierre-Marie de Rodat]

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

There is no impact on compilation.

Tested on x86_64-pc-linux-gnu, committed on trunk

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

gcc/ada/

        * sem_spark.adb (Get_Perm_Or_Tree): Issue an error when
        encountering unknown global variable.
--- gcc/ada/sem_spark.adb
+++ 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;