diff options
| author | Yannick Moy <moy@adacore.com> | 2019-07-09 07:53:26 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2019-07-09 07:53:26 +0000 |
| commit | e5ce97d294608b4918b3809bc461052b58de8993 (patch) | |
| tree | 7936c545031f86a42cc5ebd42f345819ae2763ed /gcc | |
| parent | e0201d823abfcbc3acadc1f78a0c94fdc8474dfe (diff) | |
| download | gcc-e5ce97d294608b4918b3809bc461052b58de8993.zip gcc-e5ce97d294608b4918b3809bc461052b58de8993.tar.gz gcc-e5ce97d294608b4918b3809bc461052b58de8993.tar.bz2 | |
[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
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/ChangeLog | 5 | ||||
| -rw-r--r-- | gcc/ada/sem_spark.adb | 11 |
2 files changed, 15 insertions, 1 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 9f6b789..0fd03b72 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,5 +1,10 @@ 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. diff --git a/gcc/ada/sem_spark.adb b/gcc/ada/sem_spark.adb index 2b19919..6f27d20 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; |