aboutsummaryrefslogtreecommitdiff
path: root/gcc/ada/sem_spark.adb
diff options
context:
space:
mode:
authorYannick Moy <moy@adacore.com>2019-08-21 08:29:47 +0000
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>2019-08-21 08:29:47 +0000
commit570d0072bdcdd0e9e7d6acb33f594c22efa24ac7 (patch)
treec4c29837ff9a4e2ddafdb2c3fa0df2423c7d9319 /gcc/ada/sem_spark.adb
parent78170c8ea108d76c9ed44b9a59546aadf64e9c3e (diff)
downloadgcc-570d0072bdcdd0e9e7d6acb33f594c22efa24ac7.zip
gcc-570d0072bdcdd0e9e7d6acb33f594c22efa24ac7.tar.gz
gcc-570d0072bdcdd0e9e7d6acb33f594c22efa24ac7.tar.bz2
[Ada] Ignore subprogram address in ownership checking
Ownership checking done as in GNATprove should ignore address of subprograms, as it applies only on objects. Now fixed. There is no impact on compilation. 2019-08-21 Yannick Moy <moy@adacore.com> gcc/ada/ * sem_spark.adb (Process_Path): Do nothing on address of subprogram. From-SVN: r274779
Diffstat (limited to 'gcc/ada/sem_spark.adb')
-rw-r--r--gcc/ada/sem_spark.adb1
1 files changed, 1 insertions, 0 deletions
diff --git a/gcc/ada/sem_spark.adb b/gcc/ada/sem_spark.adb
index f99dced..a246482 100644
--- a/gcc/ada/sem_spark.adb
+++ b/gcc/ada/sem_spark.adb
@@ -5110,6 +5110,7 @@ package body Sem_SPARK is
-- in an object.
if not Present (Root)
+ or else not Is_Object (Root)
or else not Is_Deep (Etype (Root))
then
return;