Enforcing Basic Program Consistency¶
Many consistency properties that are taken for granted in other languages are not enforced in C. The basic property that all uses of a variable or function agree on its type is both not enforced by the language and very difficult to enforce by a tool. Three features of C contribute to that situation:
- the textual-based inclusion of files means that every included declaration is subject to a possibly different reinterpretation.
- the lack of consistency requirements across translation units means that type inconsistencies can only be detected at link time, something linkers are ill-equipped to do.
- the default that consists in making a declaration externally visible means that programmer oversight will promote local declarations to be visible to the rest of the program, increasing the chances for inconsistencies.
MISRA-C contains guidelines on all three fronts to enforce basic program consistency.
Taming Text-Based Inclusion¶
The text-based inclusion of files is among the dated oddities of the C programming language that were inherited by C++ and that are known to cause quality problems, especially during maintenance. Although multiple inclusion of a file in the same translation unit can be used to emulate template programming, it's in general undesirable, so much that MISRA-C defines Directive 4.10 precisely to forbid it for header files: "Precautions shall be taken in order to prevent the contents of a header file being included more than once".
It follows with a specific section on "Preprocessing Directives" containing 14 rules restricting the use of text-based inclusion through preprocessing, forbidding in particular the use of #undef directive (used to work around conflicts in macro definitions introduced by text-based inclusion) and enforcing the well-known practice that macro arguments should be parenthesized (to avoid syntactic reinterpretations in the context of the macro use).
SPARK does not suffer from these problems, as it relies on semantic inclusion
of context instead of textual inclusion of content, using
with clauses are only allowed at the beginning of files, and
the compiler issues an error if they are used elsewhere:
procedure Hello_World is with Ada.Text_IO; begin Ada.Text_IO.Put_Line ("hello, world!"); end Hello_World;
Importing a unit multiple times is harmless, as it is equivalent to importing
it once, but a compiler warning lets us know about the redundant
The order in which units are imported is irrelevant. All orders are valid and
have the same semantics. There is no possible conflict as a result of importing
units, as each imported unit serves as namespace for the entities which it
defines. So we can define our own version of
Put_Line in some
unit and import it together with the standard version defined in
The only possible conflict arises if we want
Put_Line to be directly
available without using the qualified name
Helper.Put_Line. We use a
use clause to make public declarations from a
unit available directly:
Here, both units
Helper define a procedure
taking a string in argument, so the compiler cannot disambiguate the direct
Put_Line and issues an error. Note that it helpfully points to
candidate declarations, so that the user can decide which qualified name to use
as in the previous two calls.
Issues arising in C as a result of text-based inclusion of files are thus completely prevented in SPARK thanks to semantic import of units. Note that the C++ committee has identified this weakness for a long time, and has finally approved the addition of modules to C++20 that add a mechanism for semantic import of units.
Going Towards Encapsulation¶
The root cause for most of the problems seen in this section stems from the lack of encapsulation in C. There is no notion of namespace that would allow files to publish their declarations without risking a conflict with other files. Thus MISRA-C discourages the use of external declarations with multiple guidelines:
- Directive 4.8 encourages to hide the definition of structure and unions in implementation files (.c files) when possible: "If a pointer to a structure or union is never dereferenced within a translation unit, then the implementation of the object should be hidden."
- Rule 8.7 forbids the use of external declarations when not needed: "Functions and objects should not be defined with external linkage if they are referenced in only one translation unit."
- Rule 8.8 forces the explicit use of keyword
staticwhen appropriate: "The static storage class specifier shall be used in all declarations of objects and functions that have internal linkage."
In SPARK, every unit is divided into a spec (.ads file) and a body (.adb
file). Only declarations from the spec are visible from other units when they
import that unit. In fact, only declarations from the visible part of the spec
private) are visible from other units.
Note the different errors on the calls to the private and body versions of
Put_Line: in the first case the compiler can locate the candidate procedure
but it is illegal to call it from
Hello_World, in the second case the
compiler does not even known about any
Body_Put_Line when compiling
SPARK also allows to define a type in the private part of a spec (so that during the compilation of client units its definition is known to the compiler, say for allocating the correct memory for a variable of such a type) while simply announcing such a declaration in the public part of the spec. This way, client code can use the type, typically through a public API, but not any specifics on the implementation of the type.
Note that it is possible to both declare a variable of type
Information_System and to get/set it through its API in procedure
Hacker, but not to access directly its