Symbolic Execution For C++ Programs

In today's world,software plays an essential role in our production and living.Along with the significance,is the growing attention paid to software security from sociaty.For those massive and safety-critical,in order to ensure its reliability,there has been various methods invented to avoid damage cause by them.Symbolic execution is an effective way of improving software quality for some specific sort of programs.Symbolic execution simulatedly execute program using con-straints of variables instead of concrete values,getting a higher coverage of path and paying less,to generate test cases automatically or to dig bugs.ShapeChecker is a symbolic execution analyzer aimming to the C programming language,using Clang as front-end,doing analizing works to LLVM intermediate representation compiled from the C source code,is able to find bugs like access violation,dangling pointer,and arith-metic overflow.As a fundamental programming language,the C++ programming language always keeps attention from researcher of static analysis due to its sensibility and vulnerability compared with competing languages.In this dissertation,we introduce a suite of mod-ification and extension to make ShapeChecker be able to analyze programs written in C++,includes· Some methods that introduces type labeling to the analyzer and use type infor-mation to help the process of symbolic execution analyzing;· Some extension of ShapeChecker's assertion language and execution state,make it possible to do symbolic execution analysis to code that includes the usage of exception-handling feature;· Some modification to memory states and memory assertion of ShapeChecker,make it able to find bugs in code that uses C++ memory management routines.After implement work in this dissertation to ShapeChecker analyzer,we success-fully enable ShapeChecker to analyze code that includes C++ features like virtual func-tion calling,run-time type info or exception handling,and to export a fine analysis result.