diff options
author | Yannick Moy <moy@adacore.com> | 2019-07-09 07:53:21 +0000 |
---|---|---|
committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2019-07-09 07:53:21 +0000 |
commit | e0201d823abfcbc3acadc1f78a0c94fdc8474dfe (patch) | |
tree | 38dc220a202f0a0adb0bb44427b607f6553b31f2 /gcc/ada/libgnat | |
parent | b5d3d113ca9c67320ed06b65c50e8e46e22b6198 (diff) | |
download | gcc-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