C Checker Reference Manual

January 1998

next section previous section current document TenDRA home page document index

1 - Introduction
1.1 - Background
1.2 - The C static checker
1.3 - About this document
2 - Configuring the Checker
3 - Type Checking
4 - Integral Types
5 - Data Flow and Variable Analysis
6 - Preprocessing checks
7 - Dialect Features
8 - Common Errors
9 - Symbol Table Dump
10 - Conditional Compilation
11 - References
A - Compilation Modes
B - Command Line Options for Portability Checking
C - Integral Type Specification
D - Summary of the pragma statements
E - Dump format specification
F - The Token Syntax
G - API checking
H - Specifying conversions using the token syntax

1 Introduction

1.1 Background

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 document.

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:

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.

Part of the TenDRA Web.
Crown Copyright © 1998.