Our tool is built on top of cqual, a C implementation of an extensible type qualifier framework [19]. In this section we describe the underlying theory and design of cqual, which has broad applicability as an extension of the C type system.