A novel symbolic execution framework for multi-procedure program analysis

Modern software systems, which are often large-scale, with multi-procedure and complex data structures, must be extremely high quality. We present a novel framework based on symbolic execution for automatic analysis of such systems and checking of properties. We provide an improved approach of the traditional symbolic execution, namely the General-Cutting symbolic execution. We change the ways of dealing with the function calls. The process of this new approach is divided into two stages. How to deal with calling context when accessing unknown input data and how to deal with the relationship between function callings are two main challenges to the General-Cutting symbolic execution algorithm. We adopt an extensible lazy initialization method and General Execution Map Cutting method to handle these problems. It can deal with arbitrary and complex input data.