diff options
| author | Piotr Trojanek <trojanek@adacore.com> | 2023-07-10 15:02:43 +0200 |
|---|---|---|
| committer | Marc Poulhiès <poulhies@adacore.com> | 2023-07-28 09:28:13 +0200 |
| commit | 39e183a6780e4f62ac356198ec8f72a817693b89 (patch) | |
| tree | 92701a1cd634e32ddef0e599a7bb039e6c627a90 /gcc/tree-ssa-loop-manip.cc | |
| parent | 5d8fc02062b36e58c9d0bd39e7c9bb286335d870 (diff) | |
| download | gcc-39e183a6780e4f62ac356198ec8f72a817693b89.zip gcc-39e183a6780e4f62ac356198ec8f72a817693b89.tar.gz gcc-39e183a6780e4f62ac356198ec8f72a817693b89.tar.bz2 | |
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.
Diffstat (limited to 'gcc/tree-ssa-loop-manip.cc')
0 files changed, 0 insertions, 0 deletions