[Ada] Refine pointer support in SPARK

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

Refine the implementation of pointer support for SPARK analysis.

There is no impact on compilation.

2019-07-03 Yannick Moy


- sem_spark.adb (Get_Observed_Or_Borrowed_Expr): New function to return go through traversal function call. (Check_Type): Consistently use underlying type. (Get_Perm): Adapt for case of elaboration code where variables are not declared in the environment. Remove incorrect handling of borrow and observe.

f8e6d133f9f [Ada] Refine pointer support in SPARK
gcc/ada/ChangeLog | 9 ++++
gcc/ada/sem_spark.adb | 111 +++++++++++++++++++++++++++-----------------------
2 files changed, 69 insertions(+), 51 deletions(-)

Upstream: gcc.gnu.org

  • Share