Modex can be used to mechanically extract verification models from implementation level C code. first developed at Bell Labs starting in 1998, and released as open-source in 2002. The model extractor is guided by a user-defined test-harness, specified in a separate file with extension ".prx". The format used in test-harness files is documented in the Manual.
For details on the theoretical background for the tool, and its installation and use, see for instance http://spinroot.com/modex.