Static Analysis Method of C Code Based on Model Checking and Defect Pattern Matching

Static code analysis is an important means to ensure the quality and safety of software code, but the existing static code analysis tools have some problems such as complex configuration, low performance, and insufficient accuracy. This paper proposes a static analysis method of C code, which combines model checking technology and defect pattern matching technology based on lexical analysis. A framework model is designed to detect whether the C code conforms to Misra C 2012 rules, and a static analysis tool is developed based on this model method to verify validity. Experimental results show that the static analysis tool based on the model framework performs well. Compared to the open source static analysis tool Cppcheck, the accuracy and performance have been greatly improved, which improves the accuracy and performance of static analysis in large-scale code scenarios.