aboutsummaryrefslogtreecommitdiff
path: root/gcc/ada/table.adb
diff options
context:
space:
mode:
authorYannick Moy <moy@adacore.com>2019-08-14 09:51:25 +0000
committerPierre-Marie de Rodat <pmderodat@gcc.gnu.org>2019-08-14 09:51:25 +0000
commit1384d88fa9d7bb81b3e37568622f6839cd28be26 (patch)
tree7a021cf20b0f4fac191756ee5fe1f3583722cbbe /gcc/ada/table.adb
parent05b77088c086863aa3e5c0456b9a0c0075e05a6d (diff)
downloadgcc-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