| commit | 39e183a6780e4f62ac356198ec8f72a817693b89 | |
| author | Piotr Trojanek <trojanek@adacore.com> | |
| Mon, 10 Jul 2023 13:02:43 +0000 (10 15:02 +0200) | ||
| committer | Marc Poulhiès <poulhies@adacore.com> | |
| Fri, 28 Jul 2023 07:28:13 +0000 (28 09:28 +0200) | ||
| tree | 92701a1cd634e32ddef0e599a7bb039e6c627a90 | treesnapshot (tar.gz zip) |
| parent | 5d8fc02062b36e58c9d0bd39e7c9bb286335d870 | commitdiff |
ada: Leave detection of missing return in functions to GNATprove
GNAT has a heuristic to warn about missing return statements in
functions. This warning was escalated to errors when operating in
GNATprove mode and SPARK_Mode was On. However, this heuristic was
imprecise and caused spurious errors. Also, it was applied after the
Push_Scope/End_Scope, so for functions acting as compilation units it
was using the wrong SPARK_Mode.
It is better to simply leave this detection to GNATprove.
gcc/ada/
* sem_ch6.adb (Check_Statement_Sequence): Only warn about missing return
statements and let GNATprove emit a check when needed.
GNAT has a heuristic to warn about missing return statements in
functions. This warning was escalated to errors when operating in
GNATprove mode and SPARK_Mode was On. However, this heuristic was
imprecise and caused spurious errors. Also, it was applied after the
Push_Scope/End_Scope, so for functions acting as compilation units it
was using the wrong SPARK_Mode.
It is better to simply leave this detection to GNATprove.
gcc/ada/
* sem_ch6.adb (Check_Statement_Sequence): Only warn about missing return
statements and let GNATprove emit a check when needed.
| gcc/ada/sem_ch6.adb | diffblobblamehistory |