[Ada] Better error messages for ownership errors in SPARK
authorYannick Moy <moy@adacore.com>
Thu, 4 Jul 2019 08:05:36 +0000 (08:05 +0000)
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>
Thu, 4 Jul 2019 08:05:36 +0000 (08:05 +0000)
commitb04fe972e31570bfb09ae398576c1c79847a9f28
tree3c006f8ab5f75e8cae48cfa092228d32de5f529f
parent4ff5aa0c05b3a42a454d76275cf7e1f17cbb7412
[Ada] Better error messages for ownership errors in SPARK

When SPARK code does not follow the ownership rules of SPARK RM 3.10,
the error message now points to a location explaining why the object has
a more restricted permission than the expected one.

There is no impact on compilation.

2019-07-04  Yannick Moy  <moy@adacore.com>

gcc/ada/

* sem_spark.adb (Explanation, Get_Expl): New functions to get
the explanation for a permission mismatch.
(Perm_Error, Perm_Mismatch, Perm_Error_Loop_Exit): Take
explanation into account for issuing a more precise error
message.
(Set_Perm_Prefixes, Set_Perm_Extensions,
Set_Perm_Extensions_Move): Pass suitable argument for the
explanation node.

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