1.1 Background

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 (tchk). The terms, TenDRA C checker and tchk are used interchangably in this document.

• 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 C 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;

• several built-in checking environments plus support for user-defined checking profiles.

1.3 About this document

• Chapter 2: Configuring the Checker describes the built-in checking modes and the design of customised environments;

• Chapters 3-8: Type Checking, Integral Types, Data Flow and Variable Analysis , Preprocessing Checks, ISO C and Other Dialects and Common Errors respectively;

• Chapter 9: The Symbol Table Dump deals with the detection of unused header files, type checking across translation units and complete standard API usage analysis;

• Chapter 10: Conditional Compilation describes the checker's approach to conditional compilation;

• Chapter 11: References lists the references used in the production of this document;

• Annex A: Checking Modes gives a description of the built-in environments;

• Annex B: Command Line Options lists the command line checking options;

• Annex C: Specifying Integral Types describes the built-in integer modes and the methods for customising them;

• Annex D: Pragma Syntax Specification;

• Annex E: Symbol Table Dump Specification;

• Annex F: Token Syntax describes the methods and syntax used to produce abstract APIs;

• Annex G: Abstract API Manipulation gives details of the ways in which TenDRA abstract APIs may be extended, combined or overriden by local declarations;

• Annex H: Specifying Conversions with Tokens.