In this thesis, we will introduce the research work on inter-procedural static analysis, including the design and implementation of the framework, the integration with interval arithmetic, the application of our inter-procedural framework.DTSJava, Defect Testing System for Java, is a general software static testing system, taking data flow analysis, abstract interpretation, model checking as theoretical foundations. In DTSJava, software defects are described as fault state machines in which states are factors of software defects and transitions are timing relations of these factors. The analysis engine of defect testing computes state transitions according to fault state machines. If factors are distributed in several functions; we say there is a inter-procedural defect. DTSJava focus on the framework of the system and can not find inter-procedual defects.In order to improve defect coverage, we present an inter-procedual analysis framework based on defect oriented function summary. Our inter-procedural framework contains extraction and application of function summaries. In our framework, we design three kind of function summary. Precondition Summary is set of conditions which may lead to an error. Postcondition Summary describes context changes to the caller. Feature Summary represents defect-related operations, such as file operation.Finally, we present an inter-procedural resource leak testing method. Experiments show our method effective and scalable. |