diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2017-11-30 19:00:23 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-30 19:00:23 -0800 |
commit | 6d740ab8167fe0f48ea78306d65e2cb8a4de2d09 (patch) | |
tree | 55af24ca0024a7a5327b936213c055eca96107cf /configure.ac | |
parent | 4c1f1cad720a94226f7834874cf59478de35b74a (diff) |
Add debugging tools for ContextMemoryManager (#1407)
This commit adds two configuration options that help debugging memory
issues with allocations in the ContextMemoryManager:
--enable/disable-valgrind: This flag enables/disables Valgrind
instrumentation of the ContextMemoryManager. Enabled by default for
debug builds if the Valgrind headers are available.
--enable/disable-context-memory-manager: This flag enables/disables the
use of the ContextMemoryManager. If the flag is disableda dummy
ContextMemoryManager is used that does single allocations instead of
chunks. The flag is enabled by default.
Diffstat (limited to 'configure.ac')
-rw-r--r-- | configure.ac | 45 |
1 files changed, 45 insertions, 0 deletions
diff --git a/configure.ac b/configure.ac index cb36c7a9d..319b8d79f 100644 --- a/configure.ac +++ b/configure.ac @@ -500,6 +500,7 @@ case "$with_build" in if test -z "${enable_tracing+set}" ; then enable_tracing=no ; fi if test -z "${enable_dumping+set}" ; then enable_dumping=yes ; fi if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi + if test -z "${enable_valgrind+set}" ; then enable_valgrind=no ; fi ;; debug) # unoptimized, debug symbols, assertions, tracing, dumping CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_DEBUG" @@ -516,6 +517,7 @@ case "$with_build" in if test -z "${enable_tracing+set}" ; then enable_tracing=yes ; fi if test -z "${enable_dumping+set}" ; then enable_dumping=yes ; fi if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi + if test -z "${enable_valgrind+set}" ; then enable_valgrind=optional ; fi ;; default) # moderately optimized, assertions, tracing, dumping CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }" @@ -533,6 +535,7 @@ case "$with_build" in if test -z "${enable_tracing+set}" ; then enable_tracing=yes ; fi if test -z "${enable_dumping+set}" ; then enable_dumping=yes ; fi if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi + if test -z "${enable_valgrind+set}" ; then enable_valgrind=no ; fi ;; competition) # maximally optimized, no assertions, no tracing, no dumping, muzzled CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_COMPETITION_MODE" @@ -550,6 +553,7 @@ case "$with_build" in if test -z "${enable_tracing+set}" ; then enable_tracing=no ; fi if test -z "${enable_dumping+set}" ; then enable_dumping=no ; fi if test -z "${enable_muzzle+set}" ; then enable_muzzle=yes ; fi + if test -z "${enable_valgrind+set}" ; then enable_valgrind=no ; fi if test -z "${user_specified_enable_or_disable_shared}"; then enable_shared=no; fi if test -z "${user_specified_enable_or_disable_static}"; then enable_static=yes; fi if test -z "${enable_static_binary+set}"; then enable_static_binary=yes ; fi @@ -645,6 +649,47 @@ if test "$enable_debug_symbols" = yes; then CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-ggdb3" fi +AC_MSG_CHECKING([whether to enable Valgrind instrumentation]) + +AC_ARG_ENABLE([valgrind], + [AS_HELP_STRING([--enable-valgrind], + [enable Valgrind instrumentation])]) + +if test -z "${enable_valgrind+set}"; then + enable_valgrind=no +fi + +AC_MSG_RESULT([$enable_valgrind]) + +if test "$enable_valgrind" != no; then + # Valgrind instrumentation is either explicitly enabled (enable_valgrind=yes) + # or enabled if available (enable_valgrind=optional) + AC_CHECK_HEADER([valgrind/memcheck.h], + [CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_VALGRIND"], + [if test "$enable_valgrind" = yes; then + AC_MSG_ERROR([Need valgrind/memcheck.h to enable Valgrind instrumentation]) + else + AC_MSG_NOTICE([valgrind/memcheck.h missing, Valgrind instrumentation disabled]) + fi + ]) +fi + +AC_MSG_CHECKING([whether to use the context memory manager]) + +AC_ARG_ENABLE([context-memory-manager], + [AS_HELP_STRING([--disable-context-memory-manager], + [do not use the context memory manager])]) + +if test -z "${enable_context_memory_manager+set}"; then + enable_context_memory_manager=yes +fi + +AC_MSG_RESULT([$enable_context_memory_manager]) + +if test "$enable_context_memory_manager" = yes; then + CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_CONTEXT_MEMORY_MANAGER" +fi + AC_MSG_CHECKING([whether to include statistics are turned on in libcvc4]) AC_ARG_ENABLE([statistics], |