diff options
author | Yannick Moy <moy@adacore.com> | 2019-07-03 08:16:01 +0000 |
---|---|---|
committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2019-07-03 08:16:01 +0000 |
commit | f4c16c58e1a91f412eae9dd6645c165a709246cb (patch) | |
tree | 121a2199f0e146ff3c0f29fc98b31943af645ab6 /gcc/genconstants.c | |
parent | abc856cf227c4a97ddb4697bb51ab0da8dba4d94 (diff) | |
download | gcc-f4c16c58e1a91f412eae9dd6645c165a709246cb.zip gcc-f4c16c58e1a91f412eae9dd6645c165a709246cb.tar.gz gcc-f4c16c58e1a91f412eae9dd6645c165a709246cb.tar.bz2 |
[Ada] Refine pointer support in SPARK
Refine the implementation of pointer support for SPARK analysis.
There is no impact on compilation.
2019-07-03 Yannick Moy <moy@adacore.com>
gcc/ada/
* 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.
From-SVN: r272981
Diffstat (limited to 'gcc/genconstants.c')
0 files changed, 0 insertions, 0 deletions