[Ada] Handle implicit moves in SPARK ownership pointer support

Programming / Compilers / GCC - pmderodat [138bc75d-0d04-0410-961f-82ee72b054a4] - 9 July 2019 07:53 EDT

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

gcc/ada/

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

Upstream: gcc.gnu.org


  • Share