Extend Rchecker for Accurate Analysis of Real Embedded Projects

Interrupt-driven programs are widely used in embedded systems, but the uncertainty of interrupt interleaved execution may produce severe data race problems. Using static analysis for data race problem detection is an effective solution, and combining static analysis with program verification can further improve the accuracy of detection. Existing methods can only detect individual programs that can be correctly compiled, and cannot be applied to real project analysis. In this paper, we extend Rchecker for accurate analysis of real embedded projects. Our method generates CBMC commands that can be used for multiple files by adding analysis of project files, automatic processing of platform features, and completion of missing information. Experiments with testing real project engineering programs show that our tool can accurately and effectively detect data race in interrupt-driven programs in large-scale real-world cases.