Physical Type Checking for C
Satish Chandra and Thomas Reps
The effectiveness of traditional type checking in C is
limited by the presence of type conversions using type
casts. Because the C standard allows arbitrary type conversions
between pointer types, neither C compilers, nor tools such as
lint, can guarantee type safety in the presence of such type
conversions. In particular, by using casts involving pointers
to structures (C structs), a programmer can interpret any memory
region to be of any desired type, further compromising C's weak
type system. Not only do type casts make programs vulnerable to type
errors, they hinder program comprehension and maintenance by
creating latent dependencies between seemingly independent
pieces of code.
To address these problems, we have developed a
stronger form of type checking for C programs, called physical
type checking. Physical type checking takes into account
the layout of C struct fields in memory . This paper describes
an inference-based physical type checking algorithm and its
implementation. Our algorithm can be used to perform static safety
checks, as well as compute useful information for software
engineering applications.
(Click here to access the paper:
PostScript,
PDF.)