A verifiable set of well-chosen coding rules could make critical software components more thoroughly analyzable, for properties that go beyond compliance with the set of rules itself. To be effective, though, the set of rules has to be small, and must be clear enough that it can easily be understood and remembered. The rules will have to be specific enough that they can be checked mechanically.
- Restrict all code to very simple control flow constructs – do not use
longjmpconstructs, and direct or indirect recursion.
- All loops must have a fixed upper-bound. It must be trivially possible for a checking tool to prove statically that a preset upper-bound on the number of iterations of a loop cannot be exceeded. If the loop-bound cannot be proven statically, the rule
is considered violated.
- Do not use dynamic memory allocation after initialization.
- No function should be longer than what can be printed on a single sheet of paper in a standard reference format with one line per statement and one line per declaration.
- The assertion density of the code should average to a minimum of two assertions per function.
- Data objects must be declared at the smallest possible level of scope.
- The return value of non-void functions must be checked by each calling function, and the validity of parameters must be checked inside each function.
- The use of the preprocessor must be limited to the inclusion of header files and simple macro definitions. Token pasting, variable argument lists (ellipses), and recursive macro calls are not allowed.
- The use of pointers should be restricted. Specifically, no more than one level of dereferencing is allowed. Pointer dereference operations may not be hidden in macro definitions or inside typedef declarations. Function pointers are not permitted.
- All code must be compiled, from the first day of development, with all compiler warnings enabled at the compiler’s most pedantic setting. All code must compile with these setting without any warnings.
Some rules might seem absurd at first (No dynamic memory allocation, really?), yet think of these in the context of a lunar lander which you can’t hotpatch on the spot. The full PDF comes with the reasoning behind these rules.