[Ada] SPARK pointer support extended to local borrowers and observers

Programming / Compilers / GCC - pmderodat [138bc75d-0d04-0410-961f-82ee72b054a4] - 3 July 2019 08:14 EDT

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

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.

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(-)

Upstream: gcc.gnu.org


  • Share