[Ada] Allow reading a borrowed object inside a call to a pledge function
authorClaire Dross <dross@adacore.com>
Mon, 19 Aug 2019 08:35:53 +0000 (08:35 +0000)
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>
Mon, 19 Aug 2019 08:35:53 +0000 (08:35 +0000)
commitef1c6c0e5499a83be7f86ccf64e3eb8814137cc9
tree81016f920eb043f5bcee222144f2c74e9403211e
parent123f02156122ea13f3bfabdef2b6385a25527158
[Ada] Allow reading a borrowed object inside a call to a pledge function

No impact on regular compilation.

2019-08-19  Claire Dross  <dross@adacore.com>

gcc/ada/

* sem_spark.ads, sem_spark.adb (Is_Pledge_Function): New
parameter of the generic. Function used to decide whether a
function is a pledge function.
(Check_Not_Borrowed): Disable check inside the second parameter
of a pledge function for the path borrowed by the first
parameter. Also disable checks for entities inside a Global
contract.

From-SVN: r274644
gcc/ada/ChangeLog
gcc/ada/sem_spark.adb
gcc/ada/sem_spark.ads