Type Region Model and Its Application in Program Static Detection

High-assurance software has become a key goal in modern software development, especially in the design of embedded kernel systems and other fields where high reliability and security are paramount. However, programming languages such as C, characterized by pointer usage, introduce complex variable relationships such as pointer aliasing. Furthermore, the support for arbitrary type conversions in C complicates program analysis, particularly in adequately characterizing the diverse relationships among variables and handling type conversion issues during program execution. To address these challenges, this paper introduces a type region model for the formal description of variable and value information. The model constructs pointer and heap memory object representations to characterize the program states of relevant variables. Based on predefined vulnerability detection rules, it subsequently detects potential defects arising from pointers, memory operations, and type conversions. The proposed static detection methodwas evaluated using the Juliet C/C++ 1.3 test suite. The experimental results demonstrate that this method achieves a favorable balance between precision and false positive rates, making it suitable for defect detection in programs of moderate complexity.