summaryrefslogtreecommitdiff
path: root/src/base
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
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')
-rw-r--r--src/base/configuration.cpp2
-rw-r--r--src/base/configuration.h2
-rw-r--r--src/base/configuration_private.h6
3 files changed, 10 insertions, 0 deletions
diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp
index 080c817a4..0400a4e4d 100644
--- a/src/base/configuration.cpp
+++ b/src/base/configuration.cpp
@@ -84,6 +84,8 @@ bool Configuration::isProfilingBuild() {
bool Configuration::isAsanBuild() { return IS_ASAN_BUILD; }
+bool Configuration::isUbsanBuild() { return IS_UBSAN_BUILD; }
+
bool Configuration::isCompetitionBuild() {
return IS_COMPETITION_BUILD;
}
diff --git a/src/base/configuration.h b/src/base/configuration.h
index fc149587b..db0cd5cde 100644
--- a/src/base/configuration.h
+++ b/src/base/configuration.h
@@ -65,6 +65,8 @@ public:
static bool isAsanBuild();
+ static bool isUbsanBuild();
+
static bool isCompetitionBuild();
static std::string getPackageName();
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