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