fix for some Mac builds

diff --git a/config/readline.m4 b/config/readline.m4
index 95783628511b0df7969cca29c7020dc9727da38e..dcf9a9c1896bd443ca9e91140090c09d3c9cd18c 100644 (file)
--- a/config/readline.m4
+++ b/config/readline.m4
@@ -5,6 +5,7 @@ AC_DEFUN([CVC4_CHECK_FOR_READLINE], [
 AC_MSG_CHECKING([whether user requested readline support])
 LIBREADLINE=
 have_libreadline=0
+readline_compentry_func_returns_charp=0
 READLINE_LIBS=
 if test "$with_readline" = no; then
   AC_MSG_RESULT([no, readline disabled by user])
@@ -58,6 +59,16 @@ else
   fi
   if test "$with_readline" = yes; then
     have_libreadline=1
+    AC_MSG_CHECKING([for type of rl_completion_entry_function])
+    AC_LANG_PUSH([C++])
+    AC_COMPILE_IFELSE([AC_LANG_PROGRAM([
+#include <readline/readline.h>
+char* foo(const char*, int) { return (char*)0; }],[
+::rl_completion_entry_function = foo;])],
+      [AC_MSG_RESULT([char* (*)(const char*, int)])
+       readline_compentry_func_returns_charp=1],
+      [AC_MSG_FAILURE([Function])])
+    AC_LANG_POP([C++])
   else
     have_libreadline=0
     READLINE_LIBS=

diff --git a/configure.ac b/configure.ac
index 4595227a434d882cba3f96e8adf50644a7cd40a2..70351681ba4432d8005fc4a26a2456aa06b4f419 100644 (file)
--- a/configure.ac
+++ b/configure.ac
@@ -891,6 +891,7 @@ fi
 AC_ARG_WITH([readline], [AS_HELP_STRING([--with-readline], [support the readline library])], [], [with_readline=check])
 CVC4_CHECK_FOR_READLINE
 AC_DEFINE_UNQUOTED([HAVE_LIBREADLINE], $have_libreadline, [Define to 1 to use libreadline])
+AC_DEFINE_UNQUOTED([READLINE_COMPENTRY_FUNC_RETURNS_CHARP], $readline_compentry_func_returns_charp, [Define to 1 if rl_completion_entry_function is declared to return pointer to char])
 AC_SUBST([READLINE_LIBS])
 
 AC_SEARCH_LIBS([clock_gettime], [rt],

diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index cdeef23ed75a276a640ecdc2a78d661bc10c7d91..7cef623e94dc12c41139d52f26e30778e9d4f3b5 100644 (file)
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -94,8 +94,12 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager,
 
 #if HAVE_LIBREADLINE
   if(d_in == cin) {
-    ::rl_readline_name = "CVC4";
+    ::rl_readline_name = const_cast<char*>("CVC4");
+#if READLINE_COMPENTRY_FUNC_RETURNS_CHARP
     ::rl_completion_entry_function = commandGenerator;
+#else /* READLINE_COMPENTRY_FUNC_RETURNS_CHARP */
+    ::rl_completion_entry_function = (Function) commandGenerator;
+#endif /* READLINE_COMPENTRY_FUNC_RETURNS_CHARP */
     ::using_history();
 
     switch(OutputLanguage lang = toOutputLanguage(d_options[options::inputLanguage])) {