diff options
author | Yannick Moy <moy@adacore.com> | 2019-08-14 09:51:25 +0000 |
---|---|---|
committer | Pierre-Marie de Rodat <pmderodat@gcc.gnu.org> | 2019-08-14 09:51:25 +0000 |
commit | 1384d88fa9d7bb81b3e37568622f6839cd28be26 (patch) | |
tree | 7a021cf20b0f4fac191756ee5fe1f3583722cbbe /gcc/ada/table.adb | |
parent | 05b77088c086863aa3e5c0456b9a0c0075e05a6d (diff) | |
download | gcc-1384d88fa9d7bb81b3e37568622f6839cd28be26.zip gcc-1384d88fa9d7bb81b3e37568622f6839cd28be26.tar.gz gcc-1384d88fa9d7bb81b3e37568622f6839cd28be26.tar.bz2 |
[Ada] Expose part of ownership checking for use in GNATprove
GNATprove needs to be able to call a subset of the ownership legality
rules from marking. This is provided by a new function
Sem_SPARK.Is_Legal.
There is no impact on compilation.
2019-08-14 Yannick Moy <moy@adacore.com>
gcc/ada/
* sem_spark.adb, sem_spark.ads (Is_Legal): New function exposed
for use in GNATprove, to test legality rules not related to
permissions.
(Check_Declaration_Legality): Extract the part of
Check_Declaration that checks rules not related to permissions.
(Check_Declaration): Call the new Check_Declaration_Legality.
(Check_Type_Legality): Rename of Check_Type. Introduce
parameters to force or not checking, and update a flag detecting
illegalities.
(Check_Node): Ignore attribute references in statement position.
From-SVN: r274454
Diffstat (limited to 'gcc/ada/table.adb')
0 files changed, 0 insertions, 0 deletions