summaryrefslogtreecommitdiff
path: root/src/base/configuration_private.h
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2019-10-11 01:09:09 -0700
committerGitHub <noreply@github.com>2019-10-11 01:09:09 -0700
commit54449d5a9bd8e0de1a32aa35895f4edae51c5e45 (patch)
tree3a0d6d45f3143fb46463da234326b0dbf77e87dc /src/base/configuration_private.h
parent91acac585b0b2bc5a3fab4466d887cfbafa35f77 (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 'src/base/configuration_private.h')
-rw-r--r--src/base/configuration_private.h6
1 files changed, 6 insertions, 0 deletions
diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h
index 3b06a9e6a..82938adb9 100644
--- a/src/base/configuration_private.h
+++ b/src/base/configuration_private.h
@@ -172,6 +172,12 @@ namespace CVC4 {
# endif /* __has_feature(address_sanitizer) */
#endif /* defined(__has_feature) */
+#ifdef CVC4_USE_UBSAN
+#define IS_UBSAN_BUILD true
+#else /* CVC4_USE_UBSAN */
+#define IS_UBSAN_BUILD false
+#endif /* CVC4_USE_UBSAN */
+
}/* CVC4 namespace */
#endif /* CVC4__CONFIGURATION_PRIVATE_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback