The Research of an Abstract Semantic Framework for Defect Detecting
This paper proposes a non-relational abstract semantic framework. It uses interval set to represent the value of numerical variables and complete lattice to represent Boolean variables and reference variables. It presents the abstract computation method of basic expressions and the nodes of control flow graph. It uses function summaries to represent the context information of function call needed by defects detecting. Based on the results of abstract computation, it uses extended state machine to define defect patterns and proposes a path-sensitive method based on dataflow analysis to detect defects. It avoids the combination explosion of full path analysis by merging the conditions of identical property state at join points in the CFG. Practical test results show that the proposed methods have features of high efficiency, low false positive and low false negative.
Wenya Tian and Linli Xu
Z. H. Yang et al., "The Research of an Abstract Semantic Framework for Defect Detecting", Advanced Materials Research, Vol. 186, pp. 536-540, 2011