Catchconv is a proof-of-concept tool that generates test cases for signed/unsigned conversion erors in binary code. Using Valgrind, Catchconv observes a Linux binary program on an example input, then generates a query for the STP decision procedure. If a signed/unsigned bug exists, STP then synthesizes new program inputs that exhibit the bug. Well, in principle, anyway. In practice we're still working on it.
A CVS snapshot, valgrind-catchconv-0.1.tar.gz, is now available for download. The snapshot includes a demo script that runs Catchconv on a tiny test case, extracts a query generated by type inference, and then uses the STP decision procedure to synthesize new test inputs. For more details, see the README file in the valgrind-catchconv-0.1.tar.gz release.