Static Analysis Of Pointer-related Path With Variable Relationship Graph And Symbolic Execution

Software testing is an essential method for guaranteeing the quality of software. Since running test cases is error-prone and inefficient, people have been exploring new approaches to software quality assurance since 1960's. Program verification tries to prove correctness of programs with strict theorem proving. However, because of the complexity of programming languages, program verification's usage is rather limited. Static program testing is an approach between program verification and test case running. Instead of compiling and running the programs in case-based testing, static testing check programs against specifications and rules so as to pick bugs out. Although static testing cannot reveal all the bugs, it can be a very helpful supplement for runtime testing.Performing static testing, the first thing we should do is to understand programs' behavior. Since pointer variables have a strong tie with memory models, they cannot simply be treated as numeric variables. How to analyze programs that contain pointers is a hard problem in static testing. The thesis proposes a new abstract model, called variable relationship graph (VRG), to depict variables' relationship in the programs. Compared with other memory models that have been proposed, VRG can extract more information from the program and is more suitable for static analysis.To evaluate a program path that contains pointer variables, the thesis explores the methods of how to evaluate paths that contains pointers and structure variables. We statically simulate the execution of program paths with variable relationship graph and symbolic execution. During this process, VRG is adjusted according to action of programs. Constraint sets are generated at the same time. A constraint solver will be used to test the satisfiability of constraint sets. With this method, common errors like dangling pointers, memory leak and uninitialized variables, can be detected. In addition, more specific errors can be detected if programs are checked against specifications.As for the implementation, we extended PAT, a path analysis tool. With the help of variable relationship graph, the improved version can deal with pointer variables and user-defined structure variables. Some program errors that cannot be detected with other static analysis tools can be detected with our tool. Finally, a small specification language is designed and a translator is implemented to help the user write more concise specifications.