[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
This commit is contained in:
parent
558241c0f7
commit
14bc12f0b1
|
@ -1,3 +1,13 @@
|
|||
2019-07-03 Yannick Moy <moy@adacore.com>
|
||||
|
||||
* 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.
|
||||
|
||||
2019-07-03 Ed Schonberg <schonberg@adacore.com>
|
||||
|
||||
* sem_ch13.adb (Build_Predicate_Functions): In a generic context
|
||||
|
|
File diff suppressed because it is too large
Load Diff
Loading…
Reference in New Issue