Allocator expressions and sub-expressions of (extension) aggregates are implicitly the source of assignments in Ada. Thus, they should be moved when of a deep type when checking ownership rules in SPARK.
There is no impact on compilation.
2019-07-09 Yannick Moy
- sem_spark.adb (Check_Expression): Handle correctly implicit assignments as part of allocators and (extension) aggregates. (Get_Root_Object): Adapt for new path expressions. (Is_Path_Expression): Return True for (extension) aggregate.
a080baa92ec [Ada] Handle implicit moves in SPARK ownership pointer support
gcc/ada/ChangeLog | 7 ++
gcc/ada/sem_spark.adb | 208 ++++++++++++++++++++++++++++++++++++++------------
2 files changed, 167 insertions(+), 48 deletions(-)