Model checking is a formal method for verifying the temporal logic properties of finite state systems. To use the technique, an abstract model is usually constructed by hand, but this approach has some weaknesses, for instance, the cost of modeling is considerably high and the artificial models are errorprone. In this paper, we present a practical method for model checking the ANSIC programs automatically. We built C2Spin, a model extractor which analyzes the C source code and extracts the PROMELA verification model from the source code, and thereby reduce the expense of modeling significantly. Then SPIN can detect various errors in the applications implemented in C mechanically using C2Spin, such as deadlock. In preliminary experiments, depending upon the models generated by C2Spin, we find a semantic bug in SPIN4.3.0 and similar livelocks in the implementation of two classic mutual exclusion algorithms written by Holzmann. The results show that C2Spin helps people test C programs more effectively and quickly.