diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-10-11 01:09:09 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-10-11 01:09:09 -0700 |
| commit | 54449d5a9bd8e0de1a32aa35895f4edae51c5e45 (patch) | |
| tree | 3a0d6d45f3143fb46463da234326b0dbf77e87dc /CMakeLists.txt | |
| parent | 91acac585b0b2bc5a3fab4466d887cfbafa35f77 (diff) | |
Add support for UBSan instrumentation (#3382)
This commit adds support for compiling CVC4 with UBSan instrumentation.
The commit also adds a dummy version of `AigBitblaster`. Previously,
when CVC4 was built without ABC, `AigBitblaster` was not fully defined
(the class was declared but the implementation was not being compiled).
This lead to missing RTTI information when compiling with UBSan
instrumentation.
Diffstat (limited to 'CMakeLists.txt')
| -rw-r--r-- | CMakeLists.txt | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt index 4cef0bc00..f8fe74130 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -66,6 +66,7 @@ option(ENABLE_GPL "Enable GPL dependencies") # > allows to detect if set by user (default: IGNORE) # > only necessary for options set for build types cvc4_option(ENABLE_ASAN "Enable ASAN build") +cvc4_option(ENABLE_UBSAN "Enable UBSan build") cvc4_option(ENABLE_ASSERTIONS "Enable assertions") cvc4_option(ENABLE_COMP_INC_TRACK "Enable optimizations for incremental SMT-COMP tracks") @@ -154,7 +155,7 @@ endif() # to cmake standards (first letter uppercase). set(BUILD_TYPES Production Debug Testing Competition) -if(ENABLE_ASAN) +if(ENABLE_ASAN OR ENABLE_UBSAN) set(CMAKE_BUILD_TYPE Debug) endif() @@ -297,6 +298,11 @@ if(ENABLE_ASAN) add_check_c_cxx_flag("-fsanitize-recover=address") endif() +if(ENABLE_UBSAN) + add_required_c_cxx_flag("-fsanitize=undefined") + add_definitions(-DCVC4_USE_UBSAN) +endif() + if(ENABLE_ASSERTIONS) add_definitions(-DCVC4_ASSERTIONS) else() |