Many vulnerability detection tools have been developed to detect vulnerabilities, but most of them only offer basic information for each detected vulnerability, which is insufficient for developers to reproduce and repair the vulnerability. We present an approach called SPDetect that uses safety properties to detect vulnerabilities and provides semantic information, including source code program expressions, about detected vulnerabilities. Each safety property defines the condition violated by one type of vulnerabilities. SPDetect uses symbolic execution to explore program paths and detect vulnerabilities by checking any violation of safety properties. To guide the symbolic execution to deep program paths that are more likely to contain vulnerabilities, we developed the novel technique of error path termination. We have designed and implemented a prototype of SPDetect for detecting vulnerabilities in C/C++ programs. Our evaluation of SPDetect on real-world programs shows that SPDetect can can detect vulnerabilities effectively and efficiently.