aboutsummaryrefslogtreecommitdiff
path: root/gcc/ada/libgnat
diff options
context:
space:
mode:
authorYannick Moy <moy@adacore.com>2019-07-09 07:53:21 +0000
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>2019-07-09 07:53:21 +0000
commite0201d823abfcbc3acadc1f78a0c94fdc8474dfe (patch)
tree38dc220a202f0a0adb0bb44427b607f6553b31f2 /gcc/ada/libgnat
parentb5d3d113ca9c67320ed06b65c50e8e46e22b6198 (diff)
downloadgcc-e0201d823abfcbc3acadc1f78a0c94fdc8474dfe.zip
gcc-e0201d823abfcbc3acadc1f78a0c94fdc8474dfe.tar.gz
gcc-e0201d823abfcbc3acadc1f78a0c94fdc8474dfe.tar.bz2
[Ada] Fix ownership checking for pointers in SPARK
Checking of the readable status of sub-expressions occurring in the target path of an assignment should occur before the right-hand-side is moved or borrowed or observed. There is no impact on compilation. 2019-07-09 Yannick Moy <moy@adacore.com> gcc/ada/ * sem_spark.adb (Check_Expression): Change signature to take an Extended_Checking_Mode, for handling read permission checking of sub-expressions in an assignment. (Check_Parameter_Or_Global): Adapt to new behavior of Check_Expression for mode Assign. (Check_Safe_Pointers): Do not analyze generic bodies. (Check_Assignment): Separate checking of the target of an assignment. From-SVN: r273266
Diffstat (limited to 'gcc/ada/libgnat')
0 files changed, 0 insertions, 0 deletions