diff options
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], |