CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs