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 are consistent with its type is not enforced by the language and is also 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 depending on context.
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 of making a declaration externally visible means that declarations that should be local will 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 one of the dated idiosyncracies of the C programming language that was inherited by C++ and that is 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 is generally undesirable. Indeed, 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".
The subsequent section on "Preprocessing Directives" contains 14
rules restricting the use of text-based inclusion through preprocessing.
Among other things these rules forbid the use of the
(which works around conflicts in macro definitions introduced by text-based
inclusion) and enforces the well-known practice of enclosing macro arguments
in parentheses (to avoid syntactic reinterpretations in the context of the
SPARK (and more generally Ada) does not suffer from these problems, as it
relies on semantic inclusion of context instead of textual inclusion of content,
with clauses are only allowed at the beginning of files;
the compiler issues an error if they are used elsewhere:
Importing a unit (i.e., specifying it in a
with clause) multiple times is
harmless, as it is equivalent to importing it once, but a compiler warning lets
us know about the redundancy:
The order in which units are imported is irrelevant. All orders are valid and have the same semantics.
No conflict arises from importing multiple units, even if the same name is
defined in several, since each 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 way a conflict can arise is if we want to be able to reference
directly, without using the qualified name
use clause makes public declarations from a
unit available directly:
Here, both units
Helper define a procedure
Put_Line taking a
String as argument, so the compiler cannot
disambiguate the direct call to
Put_Line and issues an error.
Here is output from AdaCore's GNAT Ada compiler:
1. with Ada.Text_IO; use Ada.Text_IO; 2. with Helper; use Helper; 3. 4. procedure Hello_World is 5. begin 6. Ada.Text_IO.Put_Line ("hello, world!"); 7. Helper.Put_Line ("hello, world!"); 8. Put_Line ("hello, world!"); -- ERROR | >>> ambiguous expression (cannot resolve "Put_Line") >>> possible interpretation at helper.ads:2 >>> possible interpretation at a-textio.ads:508 9. end Hello_World;
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 (and Ada) thanks to semantic import of units. Note that the C++ committee identified this weakness some time ago and has approved the addition of modules to C++20, which provide a mechanism for semantic import of units.
Going Towards Encapsulation¶
Many problems in C stem from the lack of encapsulation. There is no notion of namespace that would allow a file to make its declarations available without risking a conflict with other files. Thus MISRA C has a number of guidelines that discourage the use of external declarations:
Directive 4.8 encourages hiding the definition of structures and unions in implementation files (
.cfiles) 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."
The basic unit of modularization in SPARK, as in Ada, is the package.
A package always has a spec (in an
.ads file), which defines the interface
to other units. It generally also has a body (in an
.adb file), which
completes the spec with an implementation. Only declarations from the package spec are
visible from other units when they import (
with) the package. In fact, only
declarations from what is called the "visible part" of the spec
(before the keyword
private) are visible from units that
with the package.
Here's the output from AdaCore's GNAT compiler:
1. with Helper; use Helper; 2. 3. procedure Hello_World is 4. begin 5. Public_Put_Line ("hello, world!"); 6. Private_Put_Line ("hello, world!"); -- ERROR | >>> "Private_Put_Line" is not visible >>> non-visible (private) declaration at helper.ads:4 7. Body_Put_Line ("hello, world!"); -- ERROR | >>> "Body_Put_Line" is undefined 8. end Hello_World;
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 know about any
Body_Put_Line when compiling
Hello_World since it only looks at the spec and not the body.
SPARK (and Ada) also allow defining a type in the private part of a package spec while
simply declaring the type name in the public ("visible") part of the spec. This way,
client code — i.e., code that
with's the package — can use the type,
typically through a public API, but have no access to how the type is implemented:
Note that it is possible to declare a variable of type
Information_System and to get/set it through its API in procedure
Hacker, but not to directly access its