False positive "Path with no return in function declared to return int" on main()

[christianhujer]

Splint version used: Splint 3.1.2

$ splint -help version
Splint 3.1.2 --- 20 Feb 2018

Maintainer: splint@packages.debian.org
Compiled using gcc -g -O2 -fstack-protector-strong -Wformat
-Werror=format-security

According to ISO/IEC 9899:TC3 (and all other versions of C known to me), it is permissible to have no return statement in main(), and if "reaching the } that terminates the main function returns a value of 0."

See http://www.open-std.org/jtc1/sc22/wg14/www/docs/n1256.pdf 5.1.2.2.3 Program termination

1 […]; reaching the } that terminates the main function returns a value of 0.

Therefore, Splint warns for no reason (according to the C specification) when encountering int main(void) and.

Example source code:

// main.c
int main(void) {
}

Expected behavior:

• Running splint main.c produces no warnings.

Actual behavior:

• Running splint main.c produces the following warning:

Splint 3.1.2 --- 20 Feb 2018

main.c: (in function main)
main.c:3:2: Path with no return in function declared to return int
  There is a path through a function declared to return a value on which there
  is no return statement. This means the execution may fall through without
  returning a meaningful result to the caller. (Use -noret to inhibit warning)

Finished checking --- 1 code warning

Workaround

A workaround is easy:

1. #include <stdlib.h>
2. Use return EXIT_SUCCESS; at the end of main().

Example:

// main.c
#include <stdlib.h>

int main(void) {
    return EXIT_SUCCESS;
}

Note: That is only true for the main() function of the hosted environment (see 5.1.2.2 Hosted environment). In case of a freestanding environment, main() is not a special function and must obey the same rules as all other functions. Splint currently has no way of distinguishing between a hosted environment and a freestanding environment, which probably is needed in order to get rid of this false positive.