Symbolic Execution with Finite State Automata

Static analysis is an essential way to find code smells and bugs because it checks the source code without execution. Moreover, static analysis can help in software engineering comprehensively, since static analysis can be used for the validation of code style, evaluate software complexity and execute code refactorings, as well. Symbolic execution is a static analysis method where the variables are interpreted with symbolic values. Clang Static Analyzer is a powerful symbolic execution engine based on the Clang compiler infrastructure that can be used with C, C++ and Objective-C. Validation of resources' usage (e.g. files, memory) requires finite state automata (FSA) for modeling the state of resource (e.g. locked or acquired resource). In this paper, we argue for an approach in which automata are in-use during the symbolic execution. In this approach, a generic automaton is used. The generic automaton can be customized for different resources. We present our domain-specific language to define automata. Our tool parses the automaton and generates checker for the symbolic execution engine. We present some generated checkers, as well.