Counterexample Guided Memory-Leak Fixing In C Programs

Recently,software application is widely used in filed like industry,agriculture,military,scientific research,etc.With the widely use of software application,software scale is more and more big and the structure is more and more complex.It is very important to ensure the correctness and normative of the program improve reliability and security of the software systems.With the rapid development of SMT solvers,model checking has been widely used in the verification of software systems in code level.Several software model checkers are developed to support the verification of software systems in large scale.One remarkable merit of model checking approach is that when a flaw is found,counterexample paths in the program that violate the desired property will be provided at the same time.C program is one of the most widely used in building software systems,and it has a flexible memory management mechanism.Many dynamically allocated memory may involved in C program,but if allocated memory chunks are not released in time after used up could cause memory leak may cause the program crash.This thesis investigates how to fix memory-leak in C programs under the guidance of counterexample paths provided by a software model checker.To do so,we first show how to automatically detect memory-leak in C programs via software model checker TPChecker,and generate all of counterexample.TPChecker ia based on the CEGAR algorithm.Second,information relative to memory allocation and usage are extracted from the counterexamples and then mapped to the proper position in the Control Flow Automaton of the program.Third,by the rules for safe memory-leak fixing,the code is repaired automatically,and generate the result file after repair.The proposed approach has been implemented in a tool named CEGFixer which works in cooperation with TPChecker to fix memory-leak in C programs,and compared with the existing memory leak repair tool Leakfix.Experiments show that the tool performs well in pratice.CEGFixer increase the rate of repair ability of C program,and more leaks type can be repaired by CEGFixer.