diff options
| author | Yannick Moy <moy@adacore.com> | 2019-07-03 08:14:52 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2019-07-03 08:14:52 +0000 |
| commit | 14bc12f0b188c847976c747e8c8389977a37187e (patch) | |
| tree | 3b9fce1972cb7ee6c136b434de165e02967781dc /gcc/ada/bindo-diagnostics.ads | |
| parent | 558241c0f71b4171c471100631af79aa93c0a9e7 (diff) | |
| download | gcc-14bc12f0b188c847976c747e8c8389977a37187e.zip gcc-14bc12f0b188c847976c747e8c8389977a37187e.tar.gz gcc-14bc12f0b188c847976c747e8c8389977a37187e.tar.bz2 | |
[Ada] SPARK pointer support extended to local borrowers and observers
SPARK rules allow local borrowers and observers to be declared. During
their lifetime, the access to the borrowed/observed object is
restricted.
There is no impact on compilation.
2019-07-03 Yannick Moy <moy@adacore.com>
gcc/ada/
* sem_spark.adb: Add support for locally borrowing and observing
a path.
(Get_Root_Object): Add parameter Through_Traversal to denote
when we are interesting in getting to the traversed parameter.
(Is_Prefix_Or_Almost): New function to support detection of
illegal access to borrowed or observed paths.
(Check_Pragma): Add analysis of assertion pragmas.
From-SVN: r272975
Diffstat (limited to 'gcc/ada/bindo-diagnostics.ads')
0 files changed, 0 insertions, 0 deletions