String Abstraction for Model Checking of C Programs