CQUAL is a type-based static analysis tool that assists programmers in
searching for bugs in C programs. CQUAL supports user-defined type qualifiers which are used in the same way as the standard C
type qualifiers such as const
.
The following code segment shows an example of a user-defined type
qualifier: unchecked
. We use this qualifier to denote a
controlled object that has not been authorized. This declaration
states that the file object (filp
) has not been checked.
struct file * $unchecked filp;
Typically, programmers specify a type qualifier lattice which
defines the sub-type relationships between qualifiers and annotate the
program with the appropriate type qualifiers. A lattice is a partially
ordered set in which all nonempty finite subsets have a least upper
bound and a greatest lower bound. For example,
Figure 3 shows a lattice with two elements,
checked
and unchecked
, and the subtype relation as
the partial order. Here it means checked
is a subtype of
unchecked
.
CQUAL has a few built-in inference rules that extend the subtype
relation to qualified types. For example, one of the rules states
that if Q1 < Q2
(meaning qualifier Q1
is a subtype of
qualifier Q2
) then type Q1 T
is a subtype of
Q2 T
for any given type T
. Replacing Q1
and
Q2
with checked
and unchecked
respectively, we
have that checked T
is a subtype of unchecked T
. From
an object-oriented programming point of view, this means that a
checked
type can be used wherever an unchecked
type
is expected, but using an unchecked
type where a checked
type is expected results in a type violation. The following code segment
shows a violation of the type hierarchy. Function func_a
expects
a checked
file pointer as its parameter, but the parameter passed
is of type unchecked
file pointer.
void func_a(struct file * $checked filp); void func_b( void ) { struct file * $unchecked filp; ... func_a(filp); ... }
Using the extended inference rules, CQUAL performs qualifier inference to detect violations against the type relations defined by the lattice. For a more detailed description of CQUAL, please refer to the original paper on CQUAL [9].