i. Introduction

The C program static checker was originally developed as a programming tool to aid the construction of portable programs using the Application Programming Interface (API) model of software portability; the principle underlying this approach being:

If a program is written to conform to an abstract API specification, then that program will be portable to any machine which implements the API specification correctly.

This approach gave the tool an unusually powerful basis for static checking of C programs and a large amount of development work has resulted in the production of the TenDRA C static checker (invoked as tcc -ch). The terms, TenDRA C checker and tcc -ch are used interchangably in this document.

Responsibilities of the C static checker are:

• strict interface checking. In particular, the checker can analyse programs against abstract APIs to check their conformance to the specification. Abstract versions of most standard APIs are provided with the tool; alternatively users can define their own abstract APIs using the syntax described in Annex G;

• checking of integer sizes, overflows and implicit integer conversions including potential 64-bit problems, against a 16 bit or 32 bit architecture profile;

• strict ISO C90 standard checking, plus configurable support for many non-ISO dialect features;

• extensive type checking, including prototype-style checking for traditionally defined functions, conversion checking, type checking on printf and scanf style argument strings and type checking between translation units;

• variable analysis, including detection of unused variables, use of uninitialised variables, dependencies on order of evaluation in expressions and detection of unused function returns, computed values and static variables;

• detection of unused header files;

• configurable tests for detecting many other common programming errors;

• Complete standard API usage analysis. No API definitions are built in to the checker; these are provided externally. A complete list of API definitions available to tcc is documented by tccenv.

• Support for user-defined checking profiles. No checking profiles are built-in to the checker; these are provided externally. A complete list of profiles exposed as -X modes to tcc as startup files is documented by tccmodes.