In this paper, we extend our earlier approach by resolving two usability issues. First, we show how to perform qualifier inference in the presence of user-defined rules by generating and solving a system of conditional set constraints, thereby relieving users of the burden of explicitly annotating programs. Second, we show how to automatically infer rules that respect a given user-defined invariant, thereby relieving qualifier designers of the burden of manually producing such rules. We have formalized both qualifier and rule inference and proven their correctness. We have also extended Clarity to support qualifier and rule inference, and we illustrate their utility in practice through experiments with several type qualifiers and open-source C programs.
[PDF | Project Page]