Sure, it’s always feasible to write secure C code: for example, using the ternary operator (cond ? : x : y;) it’s possible to write statements so that errors are thrown whenever type mismatches are found at compile time, but it also would be very easy to accidentally bypass these software constructs. However, and for serious undertakings, it’s always better to rely on the existing tools that automate the many mind-numbing tasks that comprise a software audit.
Static code analysis features a long history (with the first lint tool dating back to 1977), but only the profusion of programmers from the last decade instructed in the paradigm of strongly-typed languages generated the expectation to get the same level of pre-execution bug detection for the weakly-typed languages. So strong is the impetus for static analysis in the C arena, that the whole Clang compiler suite is replacing gcc just because is almost impossible to develop static analysis tools for it. Nowadays, in the hall of fame for static analysis code auditing software tools, Deputy gets the top prize for the open source/free program, and Coverity for the commercial one, with Veracode being a strong-contender.
Coverity is a commercial spin-off of the academic work of Dawson Engler, whose papers are a must to not only understand how their tools work, but also other cutting-edge research subjects like symbolic execution. Coverity Static Analysis generates a higher number of false positives than Veracode’s, especially given that they charge so much, but neither of the two surpass the huge number that gets generated by the venerable PC-Lint. But this last one, and others like PVS-Studio and Parasoft C/C++ are still a must if you prefer on-premise software rather than giving away to the cloud your precious source code. Or if no external tools are available, at least consider the code analysis tool in Visual Studio.
On a different category, Deputy is an innovative software project that tries to introduce rigorous type safety based on annotations that are included within the code. I agree that it’s always a great idea to start introducing annotations whenever the codebase is in a nascent state, but it’s much more cumbersome whenever software projects are in an advanced state because it is akin to the tedious maintenance of code written by others. It also features runtime checks to detect those faults that couldn’t be detected at compile time. Or if having limited time available, you may consider just using splint instead of annotating everything.
At the end, I like to think that the most critical parts of the code should be minimized and subjected to formal verification efforts (see L4.verified) but always noting the implicit circular paradox of having to write a specification for the formal verification process, which is a just a program in itself. Because, who verifies the verifier?