diff options
| author | Yannick Moy <moy@adacore.com> | 2019-07-10 09:00:48 +0000 |
|---|---|---|
| committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2019-07-10 09:00:48 +0000 |
| commit | 74b96685bb00766f8931c95d45d6e2c4d719cf1a (patch) | |
| tree | c6d62cb0553dd1c03f98c9d4090d3d85718f21ac /gcc/ada/env.c | |
| parent | 5a6446841aa17a717f2f04ec22e507c86c864355 (diff) | |
| download | gcc-74b96685bb00766f8931c95d45d6e2c4d719cf1a.zip gcc-74b96685bb00766f8931c95d45d6e2c4d719cf1a.tar.gz gcc-74b96685bb00766f8931c95d45d6e2c4d719cf1a.tar.bz2 | |
[Ada] Fix crashes on ownership checking in SPARK
Code that violates the conditions for ownership checking should lead to
error messages pointing to the violations instead of crashes.
There is no impact on compilation, only GNATprove.
2019-07-10 Yannick Moy <moy@adacore.com>
gcc/ada/
* sem_spark.adb (Get_Root_Object): Replace precondition by error
message.
(Read_Indexes): Replace precondition by error message.
(Check_Callable_Body): Check only traversal function returns an
anonymous access type.
(Check_Expression): Issue error on unexpected expression as
path.
* sem_util.adb (First_Global): Fix access to global on
entry/task.
From-SVN: r273329
Diffstat (limited to 'gcc/ada/env.c')
0 files changed, 0 insertions, 0 deletions