2.1 System Architecture

Figure 2 shows the structure of the cqual tool. The main input to the tool is the preprocessed C code the user wishes to analyze. The user also provides two types of configuration files to customize cqual to the particular checking task. The lattice file describes the type qualifiers the user is interested in (Sections 2.2 and  2.3). The prelude files contain annotated function declarations that override the declarations in the source being analyzed.

Figure 2: The architecture of the cqual system. The C source code and the configuration files are parsed, producing an annotated Abstract Syntax Tree (AST). cqual traverses the AST to generate a system (or database) of type constraints, which are solved on-line. Warnings are produced whenever an inconsistent constraint is generated. The analysis results are presented to the programmer in an emacs-based GUI, which interactively queries the constraint solver to help the user determine the cause of any error messages.

Given preprocessed C code and configuration files, cqual performs type inference on the program (Section 2.4). Finally, the results of the type inference phase are presented to the user interactively using Program Analysis Mode (PAM) for emacs (Section 3).

The configuration files make cqual usable ``out-of-the-box,'' i.e., without making any changes to the source except preprocessing. We were able to analyze all of our benchmark programs with the same standard prelude file and, in virtually all cases, no direct changes to the application source code. Typically, a few application-specific entries were added to a special local prelude file, to improve accuracy in the presence of wrappers around library functions (though the GUI indicates which ones to add). This goes a long way toward making cqual an easily usable tool.