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.
The tool was designed to address the problem of the lack of separation
between an API specification and an API implementation and as such
was considered as a compiler for an abstract machine.
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
1.2 The C static checker
The C static checker is a powerful and flexible tool which can perform
a number of static checks on C programs, including:
- 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
- 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
- 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
- complete standard API usage analysis;
- several built-in checking environments plus support for user-defined
1.3 About this document
This document is designed as a reference manual detailing the features
of the C static checker. It contains eleven chapters (including this
introduction) and nine annexes.
- 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
- 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
- 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.
Part of the TenDRA Web.
Copyright © 1998.