MISRA C is a well-known subset of C targeting critical systems. It defines around 150 rules that should be obeyed by developments in the C programming language for critical systems. Its third issue in 2012 is a notable step forwards, with much more precise description of the rules, rationales for these rules, examples of violations, and various axes along which rules are classified. One such axis is the divide between Decidable and Undecidable rules, which is defined as follows:

    A rule is decidable if it is possible for a program to answer the question with a “yes” or a “no” in every case and undecidable otherwise.

It is therefore not surprising that almost all MISRA C rule checkers, at the notable exception of PolySpace C Verifier, focus almost exclusively on decidable rules. To put it bluntly, it is just too hard to verify those 27 undecidable rules on C programs. This is why it's interesting to consider how we would verify these unverifiable rules in the SPARK 2014 subset of Ada.

In the following, I group these 27 undecidable rules by categories, and I describe how each rule would be handled in SPARK 2014.

DETERMINISTIC BEHAVIOR

Rule 1.2 Language extensions should not be used

C is well-known for the many incompatible extensions introduced by its compilers. Porting from one compiler to another is greatly facilitated if such extensions are avoided. The same holds true to a lesser degree in Ada, where compilers are free to introduce their own pragmas, attributes and aspects. GNAT helps with portability by defining restrictions No_Implementation_Pragmas, No_Implementation_Attributes and No_Implementation_Aspect_Specifications, which forbid the use of implementation-defined pragmas, attributes and aspects.

Rule 13.1 Initializer lists shall not contain persistent side effects

Rule 13.2 The value of an expression and its persistent side effects shall be the same under all permitted evaluation orders

Rule 13.5 The right hand operand of a logical && or || operator shall not contain persistent side effects

In C and in Ada, it is not specified in which order the sub-expressions of an expression are evaluated. If two sub-expressions of an expression write to the same variable, or one writes and the other reads the same variable, then the result of the evaluation will depend on the order of evaluation between these two sub-expressions, which is highly undesirable. In SPARK 2014, expressions cannot have side-effects, so the above rules hold by language design.

ABSENCE OF RUN-TIME ERRORS

Rule 1.3 There shall be no occurrence of undefined or critical unspecified behaviour

Rule 12.2 The right hand operand of a shift operator shall lie in the range zero to one less than the width in bits of the essential type of the left hand operand

The C langage is famous for its lack of checking at run time. Instead, erroneous executions trigger what the C standard calls undefined or unspecified behavior: essentially anything can happen. Ada on the contrary is famous for its strict checking at run time to detect errors. The formal verification tool GNATprove that applies to SPARK 2014 programs allows checking statically that run-time errors cannot happen.

Rule 9.1 The value of an object with automatic storage duration shall not be read before it has been set

Reading uninitialized variables is a special kind of errors that easily goes undetected in C. GNATprove allows checking statically that no uninitialized variable is read in SPARK 2014 programs.

Rule 17.2 Functions shall not call themselves, either directly or indirectly

It is common in critical software to forbid recursion, to avoid the risk of infinite recursion, or stack overflow due to too many recursive calls. Because SPARK 2014 forbids calls through pointers, the rule Recursive Subprograms can be used in the coding standard checker GNATcheck to detect all cases direct and indirect recursion in SPARK 2014.

Rule 22.2 A block of memory shall only be freed if it was allocated by means of a Standard Library function

Use of dynamically allocated pointers results in potential memory leaks, or double-free errors. Pointers are not allowed in SPARK 2014, hence no such problems can arise.

Rule 22.3 The same file shall not be open for read and write access at the same time on different streams

The interface between the software and the external world (the file system here) requires special care, as this is not under the software control. The same error could happen in SPARK 2014 and in MISRA C here.

Rule 22.4 There shall be no attempt to write to a stream which has been opened as read-only

API constraints of this kind can be captured easily with preconditions on standard library subprograms. GNATprove allows checking statically that a SPARK 2014 program does not violate subprogram preconditions.

Rule 22.5 A pointer to a FILE object shall not be dereferenced

Rule 22.6 The value of a pointer to a FILE shall not be used after the associated stream has been closed

The type FILE in C is publicly defined in the header file stdio.h, which allows dereferencing and copying it without restreint, causing possible violations of its abstraction. In Ada, the type File_Type is defined as a limited private type in unit Ada.Text_IO, which makes it impossible to either copy it or to access its components.

DETECTION OF INCONSISTENCIES

Rule 2.1 A project shall not contain unreachable code

Rule 2.2 There shall be no dead code

MISRA C defines unreachable code as code that cannot be executed (the equivalent of dead codeor deactivated code in the avionics standard DO-178), and dead code as code that does not participate in the program behavior (somehwat related to unintended functionality in DO-178). GNATprove allows detecting some (possibly not all) unreachable code and dead code through its dataflow analysis, which issues warnings on useless assignments or statements which have no effect.

Rule 14.1 A loop counter shall not have essentially floating type

Using floating-point types to simulate integers is a very bad idea, and any coding standard for critical software should ban this form of programming. In C, the existence of implicit type conversions between int and float (or double) makes it easy to slip. In Ada, this use is discouraged by the need to introduce explicit type convertions to convert an integer value into a floating-point one.

Rule 14.2 A for loop shall be well-formed

In their full generality, for loops in C can be totally unreadable. This restriction aims at restricting their use to readable for loops. For loops in Ada are already more readable than the MISRA C restricted for loops.

Rule 14.3 Controlling expressions shall not be invariant

The test of a loop should not always evaluate to true, for the loop to terminate. GNATprove allows proving that loops in SPARK 2014 programs always terminate. The test of a loop or branch should also not always evaluate to false, or else some code become unreachable. GNATprove does not currently allow detecting this error, although it could implement some form of dead code analysis like was done in SPARK 2005 toolset.

Rule 17.8 A function parameter should not be modified

C considers function parameters as local variables, which is a source of confusion for programmers. Ada clearly separates parameters which may be only read (in parameters) from parameters which may be only written (out parameters) and from parameters which may be both read and written (in out parameters), so no confusion arises in Ada.

STRONG TYPING

Rule 8.13 A pointer should point to a const-qualified type whenever possible

In C, the only way to pass parameters by reference in a call is to pass them through pointers. If this parameter should only be read, the only way to state it statically is to give it a type pointer to const-qualified type. In Ada, the same objective is achieved by using an in parameter of a by-reference type. GNATprove issues warnings on parameters that are in out but should be in because they cannot be written directly or indirectly in the subprogram.

Rule 17.5 The function argument corresponding to a parameter declared to have an array type shall have an appropriate number of elements

There are no true array types in C, only an array syntax for pointers. In Ada, array types carry their bounds, so the rule holds by language design.

Rule 18.1 A pointer resulting from arithmetic on a pointer operand shall address an element of the same array as that pointer operand

Rule 18.2 Subtraction between pointers shall only be applied to pointers that address elements of the same array

Rule 18.3 The relational operators >, >=, < and <= shall not be applied to objects of pointer type except where they point into the same object

Pointer arithmetic in C is a source of subtle bugs. No such issues arise in Ada, which forbids pointer arithmetic.

Rule 18.6 The address of an object with automatic storage shall not be copied to another object that persists after the first object has ceased to exist

The simple typing rules for pointers in C do not protect against escaping the address of a local object. Ada accessibility rules give this protection, by a combination of compile-time and run-time checks. SPARK 2014 forbids taking explicitly the address of an object on the stack, so the rule holds by language design in SPARK 2014.

Rule 19.1 An object shall not be assigned or copied to an overlapping object

Address and pointer manipulations in C easily allow corrupting the state of an object. Ada strong typing makes it very visible, for example by requiring the user to perform various calls to Unchecked_Conversion between incompatible types or addresses. Overlapping assignments in Ada (for example when copying from an array into itself using the slice syntax) simply work correctly; they do not introduce any possibility of memory corruption.

CONCLUSION

So, to summarize:

• Ada (with GNAT) gives a solution to 12 of these undecidable problems (8 completely, 4 partially)
• SPARK 2014 (with GNATprove) gives a solution to 14 more of these undecidable problems (12 completely, 2 partially)
• only one of these undecidable problems is a potential issue in SPARK 2014

The conclusion that I draw from this little matching game is that, if you care about MISRA C rules, and if there is an Ada compiler for your target (processor + operating system), you should seriously consider using SPARK 2014.