| With the development of computer software,the number and scale of software is constantly increasing.Manual test as a traditional method have many disadvantages,such as low efficiency,higher cost,etc.There are some new and automated methods which have been used to analysis program defect.Program analysis is one of defect analysis methods,which has been studied and used in the academic and industrial field.At present,these technologies have gradually replaced the traditional way.Based on whether the program will be running,program analysis can be divided into dynamic program analysis and static program analysis.Dynamic program analysis technique according to the assembly code of the target program instrument some instructions to target program or run the target program in the virtual machine to analyze the program.While static program analysis technique does not run the program,it processes on source code or intermediate code which was generated by a compiler frontend.Some methods are used to do some static analysis,including control flow analysis,data flow analysis,model checking,taint analysis and symbolic execution,each of which has advantages and disadvantages.In this paper we use static program analysis to check the defect of program,using symbolic execution technology and SMT solver to present a static analysis tool MLSA.MLSA uses LLVM IR(intermediate representation)as the analysis input,symbolic execution is used to record the value of variables with symbols,and for the checking instructions and branch instructions the SMT solver is used to determine whether the program existing defects and the path can be reached or not.MLSA as a static analysis tool support intraprocedural analysis and interprocedural analysis,now mainly for checking divided zero error,pointer overflow and dead code in C++ language,also can analyze divided zero and arrary overflow defects in Fortran.Experiments show that MLSA has the ability to analyze these program defects in real tools. |
PDF Full Text Request