The C programming language belongs to the category of imperative programming languages. It has existed for more than 30 years and is widely used nowadays for a large variety of applications. It was standardized in 1989 as ANSI C (formally ANSI X3.159-1989), and adopted by ISO in 1990 (formally ISO/CEI 9899:1990), and a new standard was created in 1999 as C ISO (formally ISO/CEI 9899:1999). C inherited features from the C++ programming language in the first ISO standard and new features of the 1999 ISO standard added dynamic arrays as well as features for intensive numerical calculus.
Among the most famous applications built with C are the UNIX operating systems, including the Linux kernel, the Microsoft Windows kernel, and the GNU gcc tool chain. C has been used extensively to make UNIX portable across several hardware platforms: For every new port, the lowest-level code is rewritten (this often consists of assembly code). The assembly code is very limited and well delimited in terms of files.
The C language can be considered a low-level or weakly typed programming language, in the sense that the data structures manipulated are close to the machine hardware: bits, bit vectors, bytes, words, long words, and pointers are manipulated frequently. Machine words can be interpreted as numbers, characters, addresses, or bit streams. Conversions between these elementary structures are made by casts, making data typing very tricky. The C language does not propose any built-in features to manipulate higher-level data structures easily (such as lists dynamically linked or not, character strings, files, etc.). The developer is, therefore, using the standard library functions to deal with such structures or additional libraries. The contrary situation exists, for instance, in Ada, with a standard that contains strong type checking and APIs to deal with high-level data structures.
Similarly, the C language provides neither any object-oriented programming means nor any exception handling mechanisms nor any concurrency means. No operator overloading is available in C, contrary to C++ or Ada, making it less friendly.
C remains valuable, however, when low-level programming has to be done, i.e., when resources have to be managed carefully. The target code produced by C compilers is also very efficient, making it the first programming language choice for embedded systems.
The C code employed in writing the Linux kernel uses the full expressivity of the C language, including not only the ANSI C set but also the gcc variant. This renders the code harder to analyze statically than other embedded applications, as you shall see. Good programming practice requires writing C code using well-defined programming rules. Rules are of a syntactic and semantic nature. Such rules are not described here as they will become explicit when the C constructs analyzed statically are described in the next sections.
As described previously, there are different categories of techniques to analyze Linux C code. For every such category, there are as many methods and specifications and proof languages as there are tools! Many tools define their own language (syntax and semantics), making specifications generally impossible to port from one tool to another.
Without a doubt, the most widely used method for analyzing C code is Hoare Logics. We will consider this method and one associated specification language as we go into the details on how to analyze the Linux C code statically. That specification language is VDM-SL (VDM stands for Vienna Development Method and SL stands for Specification Language), which was chosen because it is one of the most expressive languages for writing specifications in Hoare Logics.
Was this article helpful?
Read how to maintain and repair any desktop and laptop computer. This Ebook has articles with photos and videos that show detailed step by step pc repair and maintenance procedures. There are many links to online videos that explain how you can build, maintain, speed up, clean, and repair your computer yourself. Put the money that you were going to pay the PC Tech in your own pocket.