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
- 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.
df177848692 [Ada] SPARK pointer support extended to local borrowers and observers
gcc/ada/ChangeLog | 10 +
gcc/ada/sem_spark.adb | 871 ++++++++++++++++++++++++++++++++++++++++----------
2 files changed, 706 insertions(+), 175 deletions(-)