C.OPEN and ANNOTATOR: Tools for On-the-Fly Model Checking C Programs