Software Static Test Research Based on Symbolic Execution

Design a C static analysis method based on analyzed symbolic execution theory.It constructs the program's Abstract syntax tree by using lexical analysis and grammatical analysis and does regular inspect for the source code in the process;then according to the function calls relationship and Abstract syntax tree to determine program analysis level and the executable path is determined by the constraint solver;eventually get the final symbolic execution results of each variable through the executable path.It is helpful for measuring code quality by regular inspecting on the source based on C language grammar.It is convenient for anglicizing the static structure of program by using SAT.The symbolic expressions,which were generated by this method can assist generating of test data and improve efficiency and quality of software test.