aboutsummaryrefslogtreecommitdiff
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
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
-rw-r--r--gcc/ada/ChangeLog5
-rw-r--r--gcc/ada/sem_spark.adb1
2 files changed, 6 insertions, 0 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index f9dcd0c..65e57ef 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,8 @@
+2019-08-21 Yannick Moy <moy@adacore.com>
+
+ * sem_spark.adb (Process_Path): Do nothing on address of
+ subprogram.
+
2019-08-21 Eric Botcazou <ebotcazou@adacore.com>
* exp_util.adb (Finalize_Address): Deal consistently with
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;