[Ada] Support chained calls to traversal functions in SPARK
authorClaire Dross <dross@adacore.com>
Tue, 17 Sep 2019 08:01:58 +0000 (08:01 +0000)
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>
Tue, 17 Sep 2019 08:01:58 +0000 (08:01 +0000)
commit77562afd5b514434c7f6cacaeb1eaaa234d19736
tree914ddecace756059e0d0c95baaf844b165e741b8
parent402b91503e266ad8337be9cf05ea967fbe4cbe3c
[Ada] Support chained calls to traversal functions in SPARK

This change only affects the SPARK toolset. In the part of semantic
analysis enforcing ownership rules for SPARK, it corrects a crash in
analysis of a declaration of a local borrower whose definition is a
chain of several calls to traversal functions.

2019-09-17  Claire Dross  <dross@adacore.com>

gcc/ada/

* sem_spark.adb (Get_Observed_Or_Borrowed_Expr): If the
definition of a local borrower contains calls to traversal
functions, the borrowed expression is the first parameter of the
first traversal function call in the definition.

From-SVN: r275785
gcc/ada/ChangeLog
gcc/ada/sem_spark.adb