missing return undetected in main()
ID0001446: This issue was created automatically from Mantis Issue 1446. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001446 | Frama-C | Kernel | public | 2013-06-13 | 2013-06-13 |
| Reporter | Jochen | Assigned To | yakobowski | Resolution | no change required |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Fluorine-20130501 | Target Version | - | Fixed in Version | - |
Description :
Running "frama-c ftest.c" on the attached program, a kernel warning about a missing return statement in function ftest() is issued, which is correct. However, no such warning is issued for main(), even if ftest() is completely commented-out. In contrast, "cc -Wall ftest.c" reports both missing returns.