about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitignore2
-rw-r--r--Makefile.config.in6
-rw-r--r--autoconf/configure.ac33
-rwxr-xr-xconfigure281
-rw-r--r--include/klee/Config/config.h.in3
-rw-r--r--lib/Core/Executor.cpp45
-rw-r--r--lib/Module/ModuleUtil.cpp37
-rw-r--r--runtime/POSIX/fd.c161
-rw-r--r--runtime/POSIX/fd.h1
-rw-r--r--runtime/POSIX/fd_32.c22
-rw-r--r--runtime/POSIX/fd_64.c16
-rw-r--r--runtime/POSIX/stubs.c7
-rw-r--r--test/Runtime/POSIX/Futimesat.c43
-rw-r--r--test/Runtime/POSIX/Openat.c18
-rw-r--r--tools/klee/Makefile3
15 files changed, 510 insertions, 168 deletions
diff --git a/.gitignore b/.gitignore
index f421d69f..fb468a14 100644
--- a/.gitignore
+++ b/.gitignore
@@ -2,6 +2,7 @@ Release/
 Release+Asserts/
 Debug/
 Debug+Asserts/
+Output/
 
 cscope.*
 
@@ -14,3 +15,4 @@ cscope.*
 *.cfg
 
 config.h
+site.exp
diff --git a/Makefile.config.in b/Makefile.config.in
index 71047e41..cd209127 100644
--- a/Makefile.config.in
+++ b/Makefile.config.in
@@ -11,6 +11,9 @@ LLVM_SRC_ROOT = @LLVM_SRC@
 # (this is *not* the same as OBJ_ROOT as defined in LLVM's Makefile.config).
 LLVM_OBJ_ROOT = @LLVM_OBJ@
 
+LLVM_VERSION_MAJOR = @LLVM_VERSION_MAJOR@
+LLVM_VERSION_MINOR = @LLVM_VERSION_MINOR@
+
 # Set this to the build mode used to build LLVM (not necessarily the same
 # as the build mode used for KLEE)
 LLVM_BUILD_MODE = @LLVM_BUILD_MODE@
@@ -26,6 +29,9 @@ PROJ_INSTALL_ROOT := @prefix@
 
 STP_ROOT := @STP_ROOT@
 
+ENABLE_METASMT := @ENABLE_METASMT@
+METASMT_ROOT := @METASMT_ROOT@
+
 ENABLE_POSIX_RUNTIME := @ENABLE_POSIX_RUNTIME@
 ENABLE_STPLOG := @ENABLE_STPLOG@
 ENABLE_UCLIBC := @ENABLE_UCLIBC@
diff --git a/autoconf/configure.ac b/autoconf/configure.ac
index dfa04e22..96d8bcfe 100644
--- a/autoconf/configure.ac
+++ b/autoconf/configure.ac
@@ -352,6 +352,39 @@ else
 fi
 
 dnl **************************************************************************
+dnl User option to enable metaSMT constraint solvers and to specify the 
+dnl the location of the metaSMT root directory
+dnl **************************************************************************
+
+AC_ARG_WITH(metasmt,
+  AS_HELP_STRING([--with-metasmt],
+    [Location of metaSMT installation directory]),,)
+
+if test X$with_metasmt = X ; then
+  AC_SUBST(ENABLE_METASMT,[[0]])
+else
+  metasmt_root=`cd $with_metasmt 2> /dev/null; pwd`
+
+  dnl AC_LANG(C++)
+  old_CPPFLAGS="$CPPFLAGS"
+  old_LDFLAGS="$LDFLAGS"  
+  CPPFLAGS="$CPPFLAGS -I$metasmt_root/include"
+  LDFLAGS="$LDFLAGS -L$metasmt_root/lib -lmetaSMT"
+  AC_CHECK_HEADERS([$metasmt_root/include/metaSMT/DirectSolver_Context.hpp $metasmt_root/include/metaSMT/frontend/QF_BV.hpp],, [
+         AC_MSG_ERROR([Unable to use $metasmt_root/include/metaSMT/DirectSolver_Context.hpp header])
+  ])
+  AC_LINK_IFELSE(
+      [AC_LANG_PROGRAM([#include $metasmt_root/include/metaSMT/frontend/QF_BV.hpp], [metaSMT::logic::QF_BV::new_bitvector(3)])],
+      [],[AC_MSG_CHECKING([for new_bitvector() in -lmetaSMT])],[AC_MSG_ERROR([Unable to link with libmetaSMT])])  
+  CPPFLAGS="$old_CPPFLAGS"
+  LDFLAGS="$old_LDFLAGS"
+
+  AC_DEFINE(SUPPORT_METASMT, 1, [Supporting metaSMT API])
+  AC_SUBST(ENABLE_METASMT,[[1]])
+  AC_SUBST(METASMT_ROOT,$metasmt_root)
+fi
+
+dnl **************************************************************************
 dnl * Check for dejagnu
 dnl **************************************************************************
 AC_PATH_PROG(RUNTEST, [runtest])
diff --git a/configure b/configure
index 837ddeec..13d141d6 100755
--- a/configure
+++ b/configure
@@ -1,6 +1,6 @@
 #! /bin/sh
 # Guess values for system-dependent variables and create Makefiles.
-# Generated by GNU Autoconf 2.68 for KLEE 0.01.
+# Generated by GNU Autoconf 2.67 for KLEE 0.01.
 #
 # Report bugs to <daniel@minormatter.com>.
 #
@@ -91,7 +91,6 @@ fi
 IFS=" ""	$as_nl"
 
 # Find who we are.  Look in the path if we contain no directory separator.
-as_myself=
 case $0 in #((
   *[\\/]* ) as_myself=$0 ;;
   *) as_save_IFS=$IFS; IFS=$PATH_SEPARATOR
@@ -217,18 +216,11 @@ IFS=$as_save_IFS
   # We cannot yet assume a decent shell, so we have to provide a
 	# neutralization value for shells without unset; and this also
 	# works around shells that cannot unset nonexistent variables.
-	# Preserve -v and -x to the replacement shell.
 	BASH_ENV=/dev/null
 	ENV=/dev/null
 	(unset BASH_ENV) >/dev/null 2>&1 && unset BASH_ENV ENV
 	export CONFIG_SHELL
-	case $- in # ((((
-	  *v*x* | *x*v* ) as_opts=-vx ;;
-	  *v* ) as_opts=-v ;;
-	  *x* ) as_opts=-x ;;
-	  * ) as_opts= ;;
-	esac
-	exec "$CONFIG_SHELL" $as_opts "$as_myself" ${1+"$@"}
+	exec "$CONFIG_SHELL" "$as_myself" ${1+"$@"}
 fi
 
     if test x$as_have_required = xno; then :
@@ -605,6 +597,8 @@ ac_includes_default="\
 ac_subst_vars='LTLIBOBJS
 LIBOBJS
 RUNTEST
+METASMT_ROOT
+ENABLE_METASMT
 STP_ROOT
 CXXCPP
 ac_ct_CXX
@@ -696,6 +690,7 @@ with_uclibc
 enable_posix_runtime
 with_runtime
 with_stp
+with_metasmt
 '
       ac_precious_vars='build_alias
 host_alias
@@ -1114,7 +1109,7 @@ Try \`$0 --help' for more information"
     $as_echo "$as_me: WARNING: you should use --build, --host, --target" >&2
     expr "x$ac_option" : ".*[^-._$as_cr_alnum]" >/dev/null &&
       $as_echo "$as_me: WARNING: invalid host type: $ac_option" >&2
-    : "${build_alias=$ac_option} ${host_alias=$ac_option} ${target_alias=$ac_option}"
+    : ${build_alias=$ac_option} ${host_alias=$ac_option} ${target_alias=$ac_option}
     ;;
 
   esac
@@ -1340,6 +1335,7 @@ Optional Packages:
   --with-runtime          Select build configuration for runtime libraries
                           (default [Release+Asserts])
   --with-stp              Location of STP installation directory
+  --with-metasmt          Location of metaSMT installation directory
 
 Some influential environment variables:
   CC          C compiler command
@@ -1421,7 +1417,7 @@ test -n "$ac_init_help" && exit $ac_status
 if $ac_init_version; then
   cat <<\_ACEOF
 KLEE configure 0.01
-generated by GNU Autoconf 2.68
+generated by GNU Autoconf 2.67
 
 Copyright (C) 2010 Free Software Foundation, Inc.
 This configure script is free software; the Free Software Foundation
@@ -1467,7 +1463,7 @@ sed 's/^/| /' conftest.$ac_ext >&5
 
 	ac_retval=1
 fi
-  eval $as_lineno_stack; ${as_lineno_stack:+:} unset as_lineno
+  eval $as_lineno_stack; test "x$as_lineno_stack" = x && { as_lineno=; unset as_lineno;}
   as_fn_set_status $ac_retval
 
 } # ac_fn_c_try_compile
@@ -1504,7 +1500,7 @@ sed 's/^/| /' conftest.$ac_ext >&5
 
     ac_retval=1
 fi
-  eval $as_lineno_stack; ${as_lineno_stack:+:} unset as_lineno
+  eval $as_lineno_stack; test "x$as_lineno_stack" = x && { as_lineno=; unset as_lineno;}
   as_fn_set_status $ac_retval
 
 } # ac_fn_c_try_cpp
@@ -1517,10 +1513,10 @@ fi
 ac_fn_c_check_header_mongrel ()
 {
   as_lineno=${as_lineno-"$1"} as_lineno_stack=as_lineno_stack=$as_lineno_stack
-  if eval \${$3+:} false; then :
+  if eval "test \"\${$3+set}\"" = set; then :
   { $as_echo "$as_me:${as_lineno-$LINENO}: checking for $2" >&5
 $as_echo_n "checking for $2... " >&6; }
-if eval \${$3+:} false; then :
+if eval "test \"\${$3+set}\"" = set; then :
   $as_echo_n "(cached) " >&6
 fi
 eval ac_res=\$$3
@@ -1587,7 +1583,7 @@ $as_echo "$as_me: WARNING: $2: proceeding with the compiler's result" >&2;}
 esac
   { $as_echo "$as_me:${as_lineno-$LINENO}: checking for $2" >&5
 $as_echo_n "checking for $2... " >&6; }
-if eval \${$3+:} false; then :
+if eval "test \"\${$3+set}\"" = set; then :
   $as_echo_n "(cached) " >&6
 else
   eval "$3=\$ac_header_compiler"
@@ -1596,7 +1592,7 @@ eval ac_res=\$$3
 	       { $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_res" >&5
 $as_echo "$ac_res" >&6; }
 fi
-  eval $as_lineno_stack; ${as_lineno_stack:+:} unset as_lineno
+  eval $as_lineno_stack; test "x$as_lineno_stack" = x && { as_lineno=; unset as_lineno;}
 
 } # ac_fn_c_check_header_mongrel
 
@@ -1637,7 +1633,7 @@ sed 's/^/| /' conftest.$ac_ext >&5
        ac_retval=$ac_status
 fi
   rm -rf conftest.dSYM conftest_ipa8_conftest.oo
-  eval $as_lineno_stack; ${as_lineno_stack:+:} unset as_lineno
+  eval $as_lineno_stack; test "x$as_lineno_stack" = x && { as_lineno=; unset as_lineno;}
   as_fn_set_status $ac_retval
 
 } # ac_fn_c_try_run
@@ -1651,7 +1647,7 @@ ac_fn_c_check_header_compile ()
   as_lineno=${as_lineno-"$1"} as_lineno_stack=as_lineno_stack=$as_lineno_stack
   { $as_echo "$as_me:${as_lineno-$LINENO}: checking for $2" >&5
 $as_echo_n "checking for $2... " >&6; }
-if eval \${$3+:} false; then :
+if eval "test \"\${$3+set}\"" = set; then :
   $as_echo_n "(cached) " >&6
 else
   cat confdefs.h - <<_ACEOF >conftest.$ac_ext
@@ -1669,7 +1665,7 @@ fi
 eval ac_res=\$$3
 	       { $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_res" >&5
 $as_echo "$ac_res" >&6; }
-  eval $as_lineno_stack; ${as_lineno_stack:+:} unset as_lineno
+  eval $as_lineno_stack; test "x$as_lineno_stack" = x && { as_lineno=; unset as_lineno;}
 
 } # ac_fn_c_check_header_compile
 
@@ -1706,7 +1702,7 @@ sed 's/^/| /' conftest.$ac_ext >&5
 
 	ac_retval=1
 fi
-  eval $as_lineno_stack; ${as_lineno_stack:+:} unset as_lineno
+  eval $as_lineno_stack; test "x$as_lineno_stack" = x && { as_lineno=; unset as_lineno;}
   as_fn_set_status $ac_retval
 
 } # ac_fn_cxx_try_compile
@@ -1743,7 +1739,7 @@ sed 's/^/| /' conftest.$ac_ext >&5
 
     ac_retval=1
 fi
-  eval $as_lineno_stack; ${as_lineno_stack:+:} unset as_lineno
+  eval $as_lineno_stack; test "x$as_lineno_stack" = x && { as_lineno=; unset as_lineno;}
   as_fn_set_status $ac_retval
 
 } # ac_fn_cxx_try_cpp
@@ -1756,10 +1752,10 @@ fi
 ac_fn_cxx_check_header_mongrel ()
 {
   as_lineno=${as_lineno-"$1"} as_lineno_stack=as_lineno_stack=$as_lineno_stack
-  if eval \${$3+:} false; then :
+  if eval "test \"\${$3+set}\"" = set; then :
   { $as_echo "$as_me:${as_lineno-$LINENO}: checking for $2" >&5
 $as_echo_n "checking for $2... " >&6; }
-if eval \${$3+:} false; then :
+if eval "test \"\${$3+set}\"" = set; then :
   $as_echo_n "(cached) " >&6
 fi
 eval ac_res=\$$3
@@ -1826,7 +1822,7 @@ $as_echo "$as_me: WARNING: $2: proceeding with the compiler's result" >&2;}
 esac
   { $as_echo "$as_me:${as_lineno-$LINENO}: checking for $2" >&5
 $as_echo_n "checking for $2... " >&6; }
-if eval \${$3+:} false; then :
+if eval "test \"\${$3+set}\"" = set; then :
   $as_echo_n "(cached) " >&6
 else
   eval "$3=\$ac_header_compiler"
@@ -1835,7 +1831,7 @@ eval ac_res=\$$3
 	       { $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_res" >&5
 $as_echo "$ac_res" >&6; }
 fi
-  eval $as_lineno_stack; ${as_lineno_stack:+:} unset as_lineno
+  eval $as_lineno_stack; test "x$as_lineno_stack" = x && { as_lineno=; unset as_lineno;}
 
 } # ac_fn_cxx_check_header_mongrel
 
@@ -1880,7 +1876,7 @@ fi
   # interfere with the next link command; also delete a directory that is
   # left behind by Apple's compiler.  We do this before executing the actions.
   rm -rf conftest.dSYM conftest_ipa8_conftest.oo
-  eval $as_lineno_stack; ${as_lineno_stack:+:} unset as_lineno
+  eval $as_lineno_stack; test "x$as_lineno_stack" = x && { as_lineno=; unset as_lineno;}
   as_fn_set_status $ac_retval
 
 } # ac_fn_cxx_try_link
@@ -1889,7 +1885,7 @@ This file contains any messages produced by compilers while
 running configure, to aid debugging if configure makes a mistake.
 
 It was created by KLEE $as_me 0.01, which was
-generated by GNU Autoconf 2.68.  Invocation command line was
+generated by GNU Autoconf 2.67.  Invocation command line was
 
   $ $0 $@
 
@@ -2147,7 +2143,7 @@ $as_echo "$as_me: loading site script $ac_site_file" >&6;}
       || { { $as_echo "$as_me:${as_lineno-$LINENO}: error: in \`$ac_pwd':" >&5
 $as_echo "$as_me: error: in \`$ac_pwd':" >&2;}
 as_fn_error $? "failed to load site script $ac_site_file
-See \`config.log' for more details" "$LINENO" 5; }
+See \`config.log' for more details" "$LINENO" 5 ; }
   fi
 done
 
@@ -2322,7 +2318,7 @@ $SHELL "$ac_aux_dir/config.sub" sun4 >/dev/null 2>&1 ||
 
 { $as_echo "$as_me:${as_lineno-$LINENO}: checking build system type" >&5
 $as_echo_n "checking build system type... " >&6; }
-if ${ac_cv_build+:} false; then :
+if test "${ac_cv_build+set}" = set; then :
   $as_echo_n "(cached) " >&6
 else
   ac_build_alias=$build_alias
@@ -2338,7 +2334,7 @@ fi
 $as_echo "$ac_cv_build" >&6; }
 case $ac_cv_build in
 *-*-*) ;;
-*) as_fn_error $? "invalid value of canonical build" "$LINENO" 5;;
+*) as_fn_error $? "invalid value of canonical build" "$LINENO" 5 ;;
 esac
 build=$ac_cv_build
 ac_save_IFS=$IFS; IFS='-'
@@ -2356,7 +2352,7 @@ case $build_os in *\ *) build_os=`echo "$build_os" | sed 's/ /-/g'`;; esac
 
 { $as_echo "$as_me:${as_lineno-$LINENO}: checking host system type" >&5
 $as_echo_n "checking host system type... " >&6; }
-if ${ac_cv_host+:} false; then :
+if test "${ac_cv_host+set}" = set; then :
   $as_echo_n "(cached) " >&6
 else
   if test "x$host_alias" = x; then
@@ -2371,7 +2367,7 @@ fi
 $as_echo "$ac_cv_host" >&6; }
 case $ac_cv_host in
 *-*-*) ;;
-*) as_fn_error $? "invalid value of canonical host" "$LINENO" 5;;
+*) as_fn_error $? "invalid value of canonical host" "$LINENO" 5 ;;
 esac
 host=$ac_cv_host
 ac_save_IFS=$IFS; IFS='-'
@@ -2389,7 +2385,7 @@ case $host_os in *\ *) host_os=`echo "$host_os" | sed 's/ /-/g'`;; esac
 
 { $as_echo "$as_me:${as_lineno-$LINENO}: checking target system type" >&5
 $as_echo_n "checking target system type... " >&6; }
-if ${ac_cv_target+:} false; then :
+if test "${ac_cv_target+set}" = set; then :
   $as_echo_n "(cached) " >&6
 else
   if test "x$target_alias" = x; then
@@ -2404,7 +2400,7 @@ fi
 $as_echo "$ac_cv_target" >&6; }
 case $ac_cv_target in
 *-*-*) ;;
-*) as_fn_error $? "invalid value of canonical target" "$LINENO" 5;;
+*) as_fn_error $? "invalid value of canonical target" "$LINENO" 5 ;;
 esac
 target=$ac_cv_target
 ac_save_IFS=$IFS; IFS='-'
@@ -2429,7 +2425,7 @@ test -n "$target_alias" &&
 
 { $as_echo "$as_me:${as_lineno-$LINENO}: checking type of operating system we're going to host on" >&5
 $as_echo_n "checking type of operating system we're going to host on... " >&6; }
-if ${klee_cv_os_type+:} false; then :
+if test "${klee_cv_os_type+set}" = set; then :
   $as_echo_n "(cached) " >&6
 else
   case $host in
@@ -2776,7 +2772,7 @@ if test -n "$ac_tool_prefix"; then
 set dummy ${ac_tool_prefix}gcc; ac_word=$2
 { $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
 $as_echo_n "checking for $ac_word... " >&6; }
-if ${ac_cv_prog_CC+:} false; then :
+if test "${ac_cv_prog_CC+set}" = set; then :
   $as_echo_n "(cached) " >&6
 else
   if test -n "$CC"; then
@@ -2816,7 +2812,7 @@ if test -z "$ac_cv_prog_CC"; then
 set dummy gcc; ac_word=$2
 { $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
 $as_echo_n "checking for $ac_word... " >&6; }
-if ${ac_cv_prog_ac_ct_CC+:} false; then :
+if test "${ac_cv_prog_ac_ct_CC+set}" = set; then :
   $as_echo_n "(cached) " >&6
 else
   if test -n "$ac_ct_CC"; then
@@ -2869,7 +2865,7 @@ if test -z "$CC"; then
 set dummy ${ac_tool_prefix}cc; ac_word=$2
 { $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
 $as_echo_n "checking for $ac_word... " >&6; }
-if ${ac_cv_prog_CC+:} false; then :
+if test "${ac_cv_prog_CC+set}" = set; then :
   $as_echo_n "(cached) " >&6
 else
   if test -n "$CC"; then
@@ -2909,7 +2905,7 @@ if test -z "$CC"; then
 set dummy cc; ac_word=$2
 { $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
 $as_echo_n "checking for $ac_word... " >&6; }
-if ${ac_cv_prog_CC+:} false; then :
+if test "${ac_cv_prog_CC+set}" = set; then :
   $as_echo_n "(cached) " >&6
 else
   if test -n "$CC"; then
@@ -2968,7 +2964,7 @@ if test -z "$CC"; then
 set dummy $ac_tool_prefix$ac_prog; ac_word=$2
 { $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
 $as_echo_n "checking for $ac_word... " >&6; }
-if ${ac_cv_prog_CC+:} false; then :
+if test "${ac_cv_prog_CC+set}" = set; then :
   $as_echo_n "(cached) " >&6
 else
   if test -n "$CC"; then
@@ -3012,7 +3008,7 @@ do
 set dummy $ac_prog; ac_word=$2
 { $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
 $as_echo_n "checking for $ac_word... " >&6; }
-if ${ac_cv_prog_ac_ct_CC+:} false; then :
+if test "${ac_cv_prog_ac_ct_CC+set}" = set; then :
   $as_echo_n "(cached) " >&6
 else
   if test -n "$ac_ct_CC"; then
@@ -3067,7 +3063,7 @@ fi
 test -z "$CC" && { { $as_echo "$as_me:${as_lineno-$LINENO}: error: in \`$ac_pwd':" >&5
 $as_echo "$as_me: error: in \`$ac_pwd':" >&2;}
 as_fn_error $? "no acceptable C compiler found in \$PATH
-See \`config.log' for more details" "$LINENO" 5; }
+See \`config.log' for more details" "$LINENO" 5 ; }
 
 # Provide some information about the compiler.
 $as_echo "$as_me:${as_lineno-$LINENO}: checking for C compiler version" >&5
@@ -3182,7 +3178,7 @@ sed 's/^/| /' conftest.$ac_ext >&5
 { { $as_echo "$as_me:${as_lineno-$LINENO}: error: in \`$ac_pwd':" >&5
 $as_echo "$as_me: error: in \`$ac_pwd':" >&2;}
 as_fn_error 77 "C compiler cannot create executables
-See \`config.log' for more details" "$LINENO" 5; }
+See \`config.log' for more details" "$LINENO" 5 ; }
 else
   { $as_echo "$as_me:${as_lineno-$LINENO}: result: yes" >&5
 $as_echo "yes" >&6; }
@@ -3225,7 +3221,7 @@ else
   { { $as_echo "$as_me:${as_lineno-$LINENO}: error: in \`$ac_pwd':" >&5
 $as_echo "$as_me: error: in \`$ac_pwd':" >&2;}
 as_fn_error $? "cannot compute suffix of executables: cannot compile and link
-See \`config.log' for more details" "$LINENO" 5; }
+See \`config.log' for more details" "$LINENO" 5 ; }
 fi
 rm -f conftest conftest$ac_cv_exeext
 { $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_exeext" >&5
@@ -3284,7 +3280,7 @@ $as_echo "$ac_try_echo"; } >&5
 $as_echo "$as_me: error: in \`$ac_pwd':" >&2;}
 as_fn_error $? "cannot run C compiled programs.
 If you meant to cross compile, use \`--host'.
-See \`config.log' for more details" "$LINENO" 5; }
+See \`config.log' for more details" "$LINENO" 5 ; }
     fi
   fi
 fi
@@ -3295,7 +3291,7 @@ rm -f conftest.$ac_ext conftest$ac_cv_exeext conftest.out
 ac_clean_files=$ac_clean_files_save
 { $as_echo "$as_me:${as_lineno-$LINENO}: checking for suffix of object files" >&5
 $as_echo_n "checking for suffix of object files... " >&6; }
-if ${ac_cv_objext+:} false; then :
+if test "${ac_cv_objext+set}" = set; then :
   $as_echo_n "(cached) " >&6
 else
   cat confdefs.h - <<_ACEOF >conftest.$ac_ext
@@ -3336,7 +3332,7 @@ sed 's/^/| /' conftest.$ac_ext >&5
 { { $as_echo "$as_me:${as_lineno-$LINENO}: error: in \`$ac_pwd':" >&5
 $as_echo "$as_me: error: in \`$ac_pwd':" >&2;}
 as_fn_error $? "cannot compute suffix of object files: cannot compile
-See \`config.log' for more details" "$LINENO" 5; }
+See \`config.log' for more details" "$LINENO" 5 ; }
 fi
 rm -f conftest.$ac_cv_objext conftest.$ac_ext
 fi
@@ -3346,7 +3342,7 @@ OBJEXT=$ac_cv_objext
 ac_objext=$OBJEXT
 { $as_echo "$as_me:${as_lineno-$LINENO}: checking whether we are using the GNU C compiler" >&5
 $as_echo_n "checking whether we are using the GNU C compiler... " >&6; }
-if ${ac_cv_c_compiler_gnu+:} false; then :
+if test "${ac_cv_c_compiler_gnu+set}" = set; then :
   $as_echo_n "(cached) " >&6
 else
   cat confdefs.h - <<_ACEOF >conftest.$ac_ext
@@ -3383,7 +3379,7 @@ ac_test_CFLAGS=${CFLAGS+set}
 ac_save_CFLAGS=$CFLAGS
 { $as_echo "$as_me:${as_lineno-$LINENO}: checking whether $CC accepts -g" >&5
 $as_echo_n "checking whether $CC accepts -g... " >&6; }
-if ${ac_cv_prog_cc_g+:} false; then :
+if test "${ac_cv_prog_cc_g+set}" = set; then :
   $as_echo_n "(cached) " >&6
 else
   ac_save_c_werror_flag=$ac_c_werror_flag
@@ -3461,7 +3457,7 @@ else
 fi
 { $as_echo "$as_me:${as_lineno-$LINENO}: checking for $CC option to accept ISO C89" >&5
 $as_echo_n "checking for $CC option to accept ISO C89... " >&6; }
-if ${ac_cv_prog_cc_c89+:} false; then :
+if test "${ac_cv_prog_cc_c89+set}" = set; then :
   $as_echo_n "(cached) " >&6
 else
   ac_cv_prog_cc_c89=no
@@ -3569,7 +3565,7 @@ if test -n "$CPP" && test -d "$CPP"; then
   CPP=
 fi
 if test -z "$CPP"; then
-  if ${ac_cv_prog_CPP+:} false; then :
+  if test "${ac_cv_prog_CPP+set}" = set; then :
   $as_echo_n "(cached) " >&6
 else
       # Double quotes because CPP needs to be expanded
@@ -3685,7 +3681,7 @@ else
   { { $as_echo "$as_me:${as_lineno-$LINENO}: error: in \`$ac_pwd':" >&5
 $as_echo "$as_me: error: in \`$ac_pwd':" >&2;}
 as_fn_error $? "C preprocessor \"$CPP\" fails sanity check
-See \`config.log' for more details" "$LINENO" 5; }
+See \`config.log' for more details" "$LINENO" 5 ; }
 fi
 
 ac_ext=c
@@ -3697,7 +3693,7 @@ ac_compiler_gnu=$ac_cv_c_compiler_gnu
 
 { $as_echo "$as_me:${as_lineno-$LINENO}: checking for grep that handles long lines and -e" >&5
 $as_echo_n "checking for grep that handles long lines and -e... " >&6; }
-if ${ac_cv_path_GREP+:} false; then :
+if test "${ac_cv_path_GREP+set}" = set; then :
   $as_echo_n "(cached) " >&6
 else
   if test -z "$GREP"; then
@@ -3760,7 +3756,7 @@ $as_echo "$ac_cv_path_GREP" >&6; }
 
 { $as_echo "$as_me:${as_lineno-$LINENO}: checking for egrep" >&5
 $as_echo_n "checking for egrep... " >&6; }
-if ${ac_cv_path_EGREP+:} false; then :
+if test "${ac_cv_path_EGREP+set}" = set; then :
   $as_echo_n "(cached) " >&6
 else
   if echo a | $GREP -E '(a|b)' >/dev/null 2>&1
@@ -3827,7 +3823,7 @@ $as_echo "$ac_cv_path_EGREP" >&6; }
 
 { $as_echo "$as_me:${as_lineno-$LINENO}: checking for ANSI C header files" >&5
 $as_echo_n "checking for ANSI C header files... " >&6; }
-if ${ac_cv_header_stdc+:} false; then :
+if test "${ac_cv_header_stdc+set}" = set; then :
   $as_echo_n "(cached) " >&6
 else
   cat confdefs.h - <<_ACEOF >conftest.$ac_ext
@@ -3957,7 +3953,7 @@ done
 for ac_header in sys/acl.h
 do :
   ac_fn_c_check_header_mongrel "$LINENO" "sys/acl.h" "ac_cv_header_sys_acl_h" "$ac_includes_default"
-if test "x$ac_cv_header_sys_acl_h" = xyes; then :
+if test "x$ac_cv_header_sys_acl_h" = x""yes; then :
   cat >>confdefs.h <<_ACEOF
 #define HAVE_SYS_ACL_H 1
 _ACEOF
@@ -3990,7 +3986,7 @@ if test -z "$CXX"; then
 set dummy $ac_tool_prefix$ac_prog; ac_word=$2
 { $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
 $as_echo_n "checking for $ac_word... " >&6; }
-if ${ac_cv_prog_CXX+:} false; then :
+if test "${ac_cv_prog_CXX+set}" = set; then :
   $as_echo_n "(cached) " >&6
 else
   if test -n "$CXX"; then
@@ -4034,7 +4030,7 @@ do
 set dummy $ac_prog; ac_word=$2
 { $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
 $as_echo_n "checking for $ac_word... " >&6; }
-if ${ac_cv_prog_ac_ct_CXX+:} false; then :
+if test "${ac_cv_prog_ac_ct_CXX+set}" = set; then :
   $as_echo_n "(cached) " >&6
 else
   if test -n "$ac_ct_CXX"; then
@@ -4112,7 +4108,7 @@ done
 
 { $as_echo "$as_me:${as_lineno-$LINENO}: checking whether we are using the GNU C++ compiler" >&5
 $as_echo_n "checking whether we are using the GNU C++ compiler... " >&6; }
-if ${ac_cv_cxx_compiler_gnu+:} false; then :
+if test "${ac_cv_cxx_compiler_gnu+set}" = set; then :
   $as_echo_n "(cached) " >&6
 else
   cat confdefs.h - <<_ACEOF >conftest.$ac_ext
@@ -4149,7 +4145,7 @@ ac_test_CXXFLAGS=${CXXFLAGS+set}
 ac_save_CXXFLAGS=$CXXFLAGS
 { $as_echo "$as_me:${as_lineno-$LINENO}: checking whether $CXX accepts -g" >&5
 $as_echo_n "checking whether $CXX accepts -g... " >&6; }
-if ${ac_cv_prog_cxx_g+:} false; then :
+if test "${ac_cv_prog_cxx_g+set}" = set; then :
   $as_echo_n "(cached) " >&6
 else
   ac_save_cxx_werror_flag=$ac_cxx_werror_flag
@@ -4240,7 +4236,7 @@ ac_compiler_gnu=$ac_cv_cxx_compiler_gnu
 { $as_echo "$as_me:${as_lineno-$LINENO}: checking how to run the C++ preprocessor" >&5
 $as_echo_n "checking how to run the C++ preprocessor... " >&6; }
 if test -z "$CXXCPP"; then
-  if ${ac_cv_prog_CXXCPP+:} false; then :
+  if test "${ac_cv_prog_CXXCPP+set}" = set; then :
   $as_echo_n "(cached) " >&6
 else
       # Double quotes because CXXCPP needs to be expanded
@@ -4356,7 +4352,7 @@ else
   { { $as_echo "$as_me:${as_lineno-$LINENO}: error: in \`$ac_pwd':" >&5
 $as_echo "$as_me: error: in \`$ac_pwd':" >&2;}
 as_fn_error $? "C++ preprocessor \"$CXXCPP\" fails sanity check
-See \`config.log' for more details" "$LINENO" 5; }
+See \`config.log' for more details" "$LINENO" 5 ; }
 fi
 
 ac_ext=cpp
@@ -4369,7 +4365,7 @@ ac_compiler_gnu=$ac_cv_cxx_compiler_gnu
 for ac_header in selinux/selinux.h
 do :
   ac_fn_cxx_check_header_mongrel "$LINENO" "selinux/selinux.h" "ac_cv_header_selinux_selinux_h" "$ac_includes_default"
-if test "x$ac_cv_header_selinux_selinux_h" = xyes; then :
+if test "x$ac_cv_header_selinux_selinux_h" = x""yes; then :
   cat >>confdefs.h <<_ACEOF
 #define HAVE_SELINUX_SELINUX_H 1
 _ACEOF
@@ -4408,7 +4404,7 @@ else
   old_CPPFLAGS="$CPPFLAGS"
   CPPFLAGS="$CPPFLAGS -I$stp_root/include"
   ac_fn_cxx_check_header_mongrel "$LINENO" "stp/c_interface.h" "ac_cv_header_stp_c_interface_h" "$ac_includes_default"
-if test "x$ac_cv_header_stp_c_interface_h" = xyes; then :
+if test "x$ac_cv_header_stp_c_interface_h" = x""yes; then :
 
 else
 
@@ -4421,7 +4417,7 @@ fi
 
   { $as_echo "$as_me:${as_lineno-$LINENO}: checking for vc_setInterfaceFlags in -lstp" >&5
 $as_echo_n "checking for vc_setInterfaceFlags in -lstp... " >&6; }
-if ${ac_cv_lib_stp_vc_setInterfaceFlags+:} false; then :
+if test "${ac_cv_lib_stp_vc_setInterfaceFlags+set}" = set; then :
   $as_echo_n "(cached) " >&6
 else
   ac_check_lib_save_LIBS=$LIBS
@@ -4455,7 +4451,7 @@ LIBS=$ac_check_lib_save_LIBS
 fi
 { $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_lib_stp_vc_setInterfaceFlags" >&5
 $as_echo "$ac_cv_lib_stp_vc_setInterfaceFlags" >&6; }
-if test "x$ac_cv_lib_stp_vc_setInterfaceFlags" = xyes; then :
+if test "x$ac_cv_lib_stp_vc_setInterfaceFlags" = x""yes; then :
   cat >>confdefs.h <<_ACEOF
 #define HAVE_LIBSTP 1
 _ACEOF
@@ -4473,11 +4469,77 @@ fi
 
 fi
 
+
+
+# Check whether --with-metasmt was given.
+if test "${with_metasmt+set}" = set; then :
+  withval=$with_metasmt;
+fi
+
+
+if test X$with_metasmt = X ; then
+  ENABLE_METASMT=0
+
+else
+  metasmt_root=`cd $with_metasmt 2> /dev/null; pwd`
+
+    old_CPPFLAGS="$CPPFLAGS"
+  old_LDFLAGS="$LDFLAGS"
+  CPPFLAGS="$CPPFLAGS -I$metasmt_root/include"
+  LDFLAGS="$LDFLAGS -L$metasmt_root/lib -lmetaSMT"
+  for ac_header in $metasmt_root/include/metaSMT/DirectSolver_Context.hpp $metasmt_root/include/metaSMT/frontend/QF_BV.hpp
+do :
+  as_ac_Header=`$as_echo "ac_cv_header_$ac_header" | $as_tr_sh`
+ac_fn_cxx_check_header_mongrel "$LINENO" "$ac_header" "$as_ac_Header" "$ac_includes_default"
+if eval test \"x\$"$as_ac_Header"\" = x"yes"; then :
+  cat >>confdefs.h <<_ACEOF
+#define `$as_echo "HAVE_$ac_header" | $as_tr_cpp` 1
+_ACEOF
+
+else
+
+         as_fn_error $? "Unable to use $metasmt_root/include/metaSMT/DirectSolver_Context.hpp header" "$LINENO" 5
+
+fi
+
+done
+
+  cat confdefs.h - <<_ACEOF >conftest.$ac_ext
+/* end confdefs.h.  */
+#include $metasmt_root/include/metaSMT/frontend/QF_BV.hpp
+int
+main ()
+{
+metaSMT::logic::QF_BV::new_bitvector(3)
+  ;
+  return 0;
+}
+_ACEOF
+if ac_fn_cxx_try_link "$LINENO"; then :
+
+else
+  { $as_echo "$as_me:${as_lineno-$LINENO}: checking for new_bitvector() in -lmetaSMT" >&5
+$as_echo_n "checking for new_bitvector() in -lmetaSMT... " >&6; }
+fi
+rm -f core conftest.err conftest.$ac_objext \
+    conftest$ac_exeext conftest.$ac_ext
+  CPPFLAGS="$old_CPPFLAGS"
+  LDFLAGS="$old_LDFLAGS"
+
+
+$as_echo "#define SUPPORT_METASMT 1" >>confdefs.h
+
+  ENABLE_METASMT=1
+
+  METASMT_ROOT=$metasmt_root
+
+fi
+
 # Extract the first word of "runtest", so it can be a program name with args.
 set dummy runtest; ac_word=$2
 { $as_echo "$as_me:${as_lineno-$LINENO}: checking for $ac_word" >&5
 $as_echo_n "checking for $ac_word... " >&6; }
-if ${ac_cv_path_RUNTEST+:} false; then :
+if test "${ac_cv_path_RUNTEST+set}" = set; then :
   $as_echo_n "(cached) " >&6
 else
   case $RUNTEST in
@@ -4604,21 +4666,10 @@ $as_echo "$as_me: WARNING: cache variable $ac_var contains a newline" >&2;} ;;
      :end' >>confcache
 if diff "$cache_file" confcache >/dev/null 2>&1; then :; else
   if test -w "$cache_file"; then
-    if test "x$cache_file" != "x/dev/null"; then
+    test "x$cache_file" != "x/dev/null" &&
       { $as_echo "$as_me:${as_lineno-$LINENO}: updating cache $cache_file" >&5
 $as_echo "$as_me: updating cache $cache_file" >&6;}
-      if test ! -f "$cache_file" || test -h "$cache_file"; then
-	cat confcache >"$cache_file"
-      else
-        case $cache_file in #(
-        */* | ?:*)
-	  mv -f confcache "$cache_file"$$ &&
-	  mv -f "$cache_file"$$ "$cache_file" ;; #(
-        *)
-	  mv -f confcache "$cache_file" ;;
-	esac
-      fi
-    fi
+    cat confcache >$cache_file
   else
     { $as_echo "$as_me:${as_lineno-$LINENO}: not updating unwritable cache $cache_file" >&5
 $as_echo "$as_me: not updating unwritable cache $cache_file" >&6;}
@@ -4650,7 +4701,7 @@ LTLIBOBJS=$ac_ltlibobjs
 
 
 
-: "${CONFIG_STATUS=./config.status}"
+: ${CONFIG_STATUS=./config.status}
 ac_write_fail=0
 ac_clean_files_save=$ac_clean_files
 ac_clean_files="$ac_clean_files $CONFIG_STATUS"
@@ -4751,7 +4802,6 @@ fi
 IFS=" ""	$as_nl"
 
 # Find who we are.  Look in the path if we contain no directory separator.
-as_myself=
 case $0 in #((
   *[\\/]* ) as_myself=$0 ;;
   *) as_save_IFS=$IFS; IFS=$PATH_SEPARATOR
@@ -5059,7 +5109,7 @@ cat >>$CONFIG_STATUS <<\_ACEOF || ac_write_fail=1
 # values after options handling.
 ac_log="
 This file was extended by KLEE $as_me 0.01, which was
-generated by GNU Autoconf 2.68.  Invocation command line was
+generated by GNU Autoconf 2.67.  Invocation command line was
 
   CONFIG_FILES    = $CONFIG_FILES
   CONFIG_HEADERS  = $CONFIG_HEADERS
@@ -5125,7 +5175,7 @@ cat >>$CONFIG_STATUS <<_ACEOF || ac_write_fail=1
 ac_cs_config="`$as_echo "$ac_configure_args" | sed 's/^ //; s/[\\""\`\$]/\\\\&/g'`"
 ac_cs_version="\\
 KLEE config.status 0.01
-configured by $0, generated by GNU Autoconf 2.68,
+configured by $0, generated by GNU Autoconf 2.67,
   with options \\"\$ac_cs_config\\"
 
 Copyright (C) 2010 Free Software Foundation, Inc.
@@ -5263,7 +5313,7 @@ do
     "tools/Makefile") CONFIG_COMMANDS="$CONFIG_COMMANDS tools/Makefile" ;;
     "unittests/Makefile") CONFIG_COMMANDS="$CONFIG_COMMANDS unittests/Makefile" ;;
 
-  *) as_fn_error $? "invalid argument: \`$ac_config_target'" "$LINENO" 5;;
+  *) as_fn_error $? "invalid argument: \`$ac_config_target'" "$LINENO" 5 ;;
   esac
 done
 
@@ -5286,10 +5336,9 @@ fi
 # after its creation but before its name has been assigned to `$tmp'.
 $debug ||
 {
-  tmp= ac_tmp=
+  tmp=
   trap 'exit_status=$?
-  : "${ac_tmp:=$tmp}"
-  { test ! -d "$ac_tmp" || rm -fr "$ac_tmp"; } && exit $exit_status
+  { test -z "$tmp" || test ! -d "$tmp" || rm -fr "$tmp"; } && exit $exit_status
 ' 0
   trap 'as_fn_exit 1' 1 2 13 15
 }
@@ -5297,13 +5346,12 @@ $debug ||
 
 {
   tmp=`(umask 077 && mktemp -d "./confXXXXXX") 2>/dev/null` &&
-  test -d "$tmp"
+  test -n "$tmp" && test -d "$tmp"
 }  ||
 {
   tmp=./conf$$-$RANDOM
   (umask 077 && mkdir "$tmp")
 } || as_fn_error $? "cannot create a temporary directory in ." "$LINENO" 5
-ac_tmp=$tmp
 
 # Set up the scripts for CONFIG_FILES section.
 # No need to generate them if there are no CONFIG_FILES.
@@ -5325,7 +5373,7 @@ else
   ac_cs_awk_cr=$ac_cr
 fi
 
-echo 'BEGIN {' >"$ac_tmp/subs1.awk" &&
+echo 'BEGIN {' >"$tmp/subs1.awk" &&
 _ACEOF
 
 
@@ -5353,7 +5401,7 @@ done
 rm -f conf$$subs.sh
 
 cat >>$CONFIG_STATUS <<_ACEOF || ac_write_fail=1
-cat >>"\$ac_tmp/subs1.awk" <<\\_ACAWK &&
+cat >>"\$tmp/subs1.awk" <<\\_ACAWK &&
 _ACEOF
 sed -n '
 h
@@ -5401,7 +5449,7 @@ t delim
 rm -f conf$$subs.awk
 cat >>$CONFIG_STATUS <<_ACEOF || ac_write_fail=1
 _ACAWK
-cat >>"\$ac_tmp/subs1.awk" <<_ACAWK &&
+cat >>"\$tmp/subs1.awk" <<_ACAWK &&
   for (key in S) S_is_set[key] = 1
   FS = ""
 
@@ -5433,7 +5481,7 @@ if sed "s/$ac_cr//" < /dev/null > /dev/null 2>&1; then
   sed "s/$ac_cr\$//; s/$ac_cr/$ac_cs_awk_cr/g"
 else
   cat
-fi < "$ac_tmp/subs1.awk" > "$ac_tmp/subs.awk" \
+fi < "$tmp/subs1.awk" > "$tmp/subs.awk" \
   || as_fn_error $? "could not setup config files machinery" "$LINENO" 5
 _ACEOF
 
@@ -5467,7 +5515,7 @@ fi # test -n "$CONFIG_FILES"
 # No need to generate them if there are no CONFIG_HEADERS.
 # This happens for instance with `./config.status Makefile'.
 if test -n "$CONFIG_HEADERS"; then
-cat >"$ac_tmp/defines.awk" <<\_ACAWK ||
+cat >"$tmp/defines.awk" <<\_ACAWK ||
 BEGIN {
 _ACEOF
 
@@ -5479,8 +5527,8 @@ _ACEOF
 # handling of long lines.
 ac_delim='%!_!# '
 for ac_last_try in false false :; do
-  ac_tt=`sed -n "/$ac_delim/p" confdefs.h`
-  if test -z "$ac_tt"; then
+  ac_t=`sed -n "/$ac_delim/p" confdefs.h`
+  if test -z "$ac_t"; then
     break
   elif $ac_last_try; then
     as_fn_error $? "could not make $CONFIG_HEADERS" "$LINENO" 5
@@ -5581,7 +5629,7 @@ do
   esac
   case $ac_mode$ac_tag in
   :[FHL]*:*);;
-  :L* | :C*:*) as_fn_error $? "invalid tag \`$ac_tag'" "$LINENO" 5;;
+  :L* | :C*:*) as_fn_error $? "invalid tag \`$ac_tag'" "$LINENO" 5 ;;
   :[FH]-) ac_tag=-:-;;
   :[FH]*) ac_tag=$ac_tag:$ac_tag.in;;
   esac
@@ -5600,7 +5648,7 @@ do
     for ac_f
     do
       case $ac_f in
-      -) ac_f="$ac_tmp/stdin";;
+      -) ac_f="$tmp/stdin";;
       *) # Look for the file first in the build tree, then in the source tree
 	 # (if the path is not absolute).  The absolute path cannot be DOS-style,
 	 # because $ac_f cannot contain `:'.
@@ -5609,7 +5657,7 @@ do
 	   [\\/$]*) false;;
 	   *) test -f "$srcdir/$ac_f" && ac_f="$srcdir/$ac_f";;
 	   esac ||
-	   as_fn_error 1 "cannot find input file: \`$ac_f'" "$LINENO" 5;;
+	   as_fn_error 1 "cannot find input file: \`$ac_f'" "$LINENO" 5 ;;
       esac
       case $ac_f in *\'*) ac_f=`$as_echo "$ac_f" | sed "s/'/'\\\\\\\\''/g"`;; esac
       as_fn_append ac_file_inputs " '$ac_f'"
@@ -5635,8 +5683,8 @@ $as_echo "$as_me: creating $ac_file" >&6;}
     esac
 
     case $ac_tag in
-    *:-:* | *:-) cat >"$ac_tmp/stdin" \
-      || as_fn_error $? "could not create $ac_file" "$LINENO" 5 ;;
+    *:-:* | *:-) cat >"$tmp/stdin" \
+      || as_fn_error $? "could not create $ac_file" "$LINENO" 5  ;;
     esac
     ;;
   esac
@@ -5761,22 +5809,21 @@ s&@abs_builddir@&$ac_abs_builddir&;t t
 s&@abs_top_builddir@&$ac_abs_top_builddir&;t t
 $ac_datarootdir_hack
 "
-eval sed \"\$ac_sed_extra\" "$ac_file_inputs" | $AWK -f "$ac_tmp/subs.awk" \
-  >$ac_tmp/out || as_fn_error $? "could not create $ac_file" "$LINENO" 5
+eval sed \"\$ac_sed_extra\" "$ac_file_inputs" | $AWK -f "$tmp/subs.awk" >$tmp/out \
+  || as_fn_error $? "could not create $ac_file" "$LINENO" 5
 
 test -z "$ac_datarootdir_hack$ac_datarootdir_seen" &&
-  { ac_out=`sed -n '/\${datarootdir}/p' "$ac_tmp/out"`; test -n "$ac_out"; } &&
-  { ac_out=`sed -n '/^[	 ]*datarootdir[	 ]*:*=/p' \
-      "$ac_tmp/out"`; test -z "$ac_out"; } &&
+  { ac_out=`sed -n '/\${datarootdir}/p' "$tmp/out"`; test -n "$ac_out"; } &&
+  { ac_out=`sed -n '/^[	 ]*datarootdir[	 ]*:*=/p' "$tmp/out"`; test -z "$ac_out"; } &&
   { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: $ac_file contains a reference to the variable \`datarootdir'
 which seems to be undefined.  Please make sure it is defined" >&5
 $as_echo "$as_me: WARNING: $ac_file contains a reference to the variable \`datarootdir'
 which seems to be undefined.  Please make sure it is defined" >&2;}
 
-  rm -f "$ac_tmp/stdin"
+  rm -f "$tmp/stdin"
   case $ac_file in
-  -) cat "$ac_tmp/out" && rm -f "$ac_tmp/out";;
-  *) rm -f "$ac_file" && mv "$ac_tmp/out" "$ac_file";;
+  -) cat "$tmp/out" && rm -f "$tmp/out";;
+  *) rm -f "$ac_file" && mv "$tmp/out" "$ac_file";;
   esac \
   || as_fn_error $? "could not create $ac_file" "$LINENO" 5
  ;;
@@ -5787,20 +5834,20 @@ which seems to be undefined.  Please make sure it is defined" >&2;}
   if test x"$ac_file" != x-; then
     {
       $as_echo "/* $configure_input  */" \
-      && eval '$AWK -f "$ac_tmp/defines.awk"' "$ac_file_inputs"
-    } >"$ac_tmp/config.h" \
+      && eval '$AWK -f "$tmp/defines.awk"' "$ac_file_inputs"
+    } >"$tmp/config.h" \
       || as_fn_error $? "could not create $ac_file" "$LINENO" 5
-    if diff "$ac_file" "$ac_tmp/config.h" >/dev/null 2>&1; then
+    if diff "$ac_file" "$tmp/config.h" >/dev/null 2>&1; then
       { $as_echo "$as_me:${as_lineno-$LINENO}: $ac_file is unchanged" >&5
 $as_echo "$as_me: $ac_file is unchanged" >&6;}
     else
       rm -f "$ac_file"
-      mv "$ac_tmp/config.h" "$ac_file" \
+      mv "$tmp/config.h" "$ac_file" \
 	|| as_fn_error $? "could not create $ac_file" "$LINENO" 5
     fi
   else
     $as_echo "/* $configure_input  */" \
-      && eval '$AWK -f "$ac_tmp/defines.awk"' "$ac_file_inputs" \
+      && eval '$AWK -f "$tmp/defines.awk"' "$ac_file_inputs" \
       || as_fn_error $? "could not create -" "$LINENO" 5
   fi
  ;;
diff --git a/include/klee/Config/config.h.in b/include/klee/Config/config.h.in
index 4ce9714d..a751bc07 100644
--- a/include/klee/Config/config.h.in
+++ b/include/klee/Config/config.h.in
@@ -78,4 +78,7 @@
 /* Define to 1 if you have the ANSI C header files. */
 #undef STDC_HEADERS
 
+/* Supporting metaSMT API */
+#undef SUPPORT_METASMT
+
 #endif
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index bef34059..caf0de36 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -572,20 +572,31 @@ void Executor::branch(ExecutionState &state,
   unsigned N = conditions.size();
   assert(N);
 
-  stats::forks += N-1;
-
-  // XXX do proper balance or keep random?
-  result.push_back(&state);
-  for (unsigned i=1; i<N; ++i) {
-    ExecutionState *es = result[theRNG.getInt32() % i];
-    ExecutionState *ns = es->branch();
-    addedStates.insert(ns);
-    result.push_back(ns);
-    es->ptreeNode->data = 0;
-    std::pair<PTree::Node*,PTree::Node*> res = 
-      processTree->split(es->ptreeNode, ns, es);
-    ns->ptreeNode = res.first;
-    es->ptreeNode = res.second;
+  if (MaxForks!=~0u && stats::forks >= MaxForks) {
+    unsigned next = theRNG.getInt32() % N;
+    for (unsigned i=0; i<N; ++i) {
+      if (i == next) {
+        result.push_back(&state);
+      } else {
+        result.push_back(NULL);
+      }
+    }
+  } else {
+    stats::forks += N-1;
+
+    // XXX do proper balance or keep random?
+    result.push_back(&state);
+    for (unsigned i=1; i<N; ++i) {
+      ExecutionState *es = result[theRNG.getInt32() % i];
+      ExecutionState *ns = es->branch();
+      addedStates.insert(ns);
+      result.push_back(ns);
+      es->ptreeNode->data = 0;
+      std::pair<PTree::Node*,PTree::Node*> res = 
+        processTree->split(es->ptreeNode, ns, es);
+      ns->ptreeNode = res.first;
+      es->ptreeNode = res.second;
+    }
   }
 
   // If necessary redistribute seeds to match conditions, killing
@@ -620,12 +631,14 @@ void Executor::branch(ExecutionState &state,
       if (i==N)
         i = theRNG.getInt32() % N;
 
-      seedMap[result[i]].push_back(*siit);
+      // Extra check in case we're replaying seeds with a max-fork
+      if (result[i])
+        seedMap[result[i]].push_back(*siit);
     }
 
     if (OnlyReplaySeeds) {
       for (unsigned i=0; i<N; ++i) {
-        if (!seedMap.count(result[i])) {
+        if (result[i] && !seedMap.count(result[i])) {
           terminateState(*result[i]);
           result[i] = NULL;
         }
diff --git a/lib/Module/ModuleUtil.cpp b/lib/Module/ModuleUtil.cpp
index 617a91ca..43eef0b7 100644
--- a/lib/Module/ModuleUtil.cpp
+++ b/lib/Module/ModuleUtil.cpp
@@ -15,6 +15,7 @@
 #include "llvm/IR/Function.h"
 #include "llvm/IR/Instructions.h"
 #include "llvm/IR/IntrinsicInst.h"
+#include "llvm/IRReader/IRReader.h"
 #include "llvm/IR/Module.h"
 #include "llvm/Support/SourceMgr.h"
 #include "llvm/Support/DataStream.h"
@@ -54,34 +55,18 @@ using namespace klee;
 Module *klee::linkWithLibrary(Module *module, 
                               const std::string &libraryName) {
 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
-  Linker linker(module);
-  std::string errorMessage;
-
-  DataStreamer * streamer = getDataFileStreamer(libraryName, &errorMessage);
-
-  if (!streamer)
-    fprintf(stderr, "Error Loading file: %s\n", errorMessage.c_str());
-  assert(streamer);
-  
-  OwningPtr<Module> library_module;
-  library_module.reset(getStreamedBitcodeModule(libraryName, streamer, getGlobalContext(), &errorMessage));
-  if (library_module.get() != 0
-	  && library_module->MaterializeAllPermanently(&errorMessage)) {
-	  library_module.reset();
+  SMDiagnostic err;
+  std::string err_str;
+  sys::Path libraryPath(libraryName);
+  Module *new_mod = ParseIRFile(libraryPath.str(), err, 
+module->getContext());
+
+  if (Linker::LinkModules(module, new_mod, Linker::DestroySource, 
+&err_str)) {
+    assert(0 && "linked in library failed!");
   }
 
-  if (library_module.get() == 0) {
-	  errs() << errorMessage << " for " << libraryName << "\n";
-	  assert(library_module.get());
-  }
-  if (linker.linkInModule(library_module.get(), &errorMessage)){
-	  fprintf(stderr, "Error in Linking %s; Existing module: %s, library to be linked in %s\n", errorMessage.c_str(),
-	      module->getModuleIdentifier().c_str(), libraryName.c_str());
-	  assert(0 && "linking in library failed!");
-  }
-
-  return linker.getModule();
-
+  return module;
 #else
   Linker linker("klee", module, false);
 
diff --git a/runtime/POSIX/fd.c b/runtime/POSIX/fd.c
index b9a848d0..09dd7be5 100644
--- a/runtime/POSIX/fd.c
+++ b/runtime/POSIX/fd.c
@@ -198,6 +198,108 @@ int __fd_open(const char *pathname, int flags, mode_t mode) {
   return fd;
 }
 
+int __fd_openat(int basefd, const char *pathname, int flags, mode_t mode) {
+  exe_file_t *f;
+  int fd;
+  if (basefd != AT_FDCWD) {
+    exe_file_t *bf = __get_file(basefd);
+
+    if (!bf) {
+      errno = EBADF;
+      return -1;
+    } else if (bf->dfile) {
+      klee_warning("symbolic file descriptor, ignoring (ENOENT)");
+      errno = ENOENT;
+      return -1;
+    }
+    basefd = bf->fd;
+  }
+
+  if (__get_sym_file(pathname)) {
+    /* for a symbolic file, it doesn't matter if/where it exists on disk */
+    return __fd_open(pathname, flags, mode);
+  }
+
+  for (fd = 0; fd < MAX_FDS; ++fd)
+    if (!(__exe_env.fds[fd].flags & eOpen))
+      break;
+  if (fd == MAX_FDS) {
+    errno = EMFILE;
+    return -1;
+  }
+  
+  f = &__exe_env.fds[fd];
+
+  /* Should be the case if file was available, but just in case. */
+  memset(f, 0, sizeof *f);
+
+  int os_fd = syscall(__NR_openat, (long)basefd, __concretize_string(pathname), (long)flags, mode);
+  if (os_fd == -1) {
+    errno = klee_get_errno();
+    return -1;
+  }
+
+  f->fd = os_fd;
+  f->flags = eOpen;
+  if ((flags & O_ACCMODE) == O_RDONLY) {
+    f->flags |= eReadable;
+  } else if ((flags & O_ACCMODE) == O_WRONLY) {
+    f->flags |= eWriteable;
+  } else { /* XXX What actually happens here if != O_RDWR. */
+    f->flags |= eReadable | eWriteable;
+  }
+
+  return fd;
+}
+
+
+int utimes(const char *path, const struct timeval times[2]) {
+  exe_disk_file_t *dfile = __get_sym_file(path);
+
+  if (dfile) {
+    /* don't bother with usecs */
+    dfile->stat->st_atime = times[0].tv_sec;
+    dfile->stat->st_mtime = times[1].tv_sec;
+#ifdef _BSD_SOURCE
+    dfile->stat->st_atim.tv_nsec = 1000000000ll * times[0].tv_sec;
+    dfile->stat->st_mtim.tv_nsec = 1000000000ll * times[1].tv_sec;
+#endif
+    return 0;
+  }
+  int r = syscall(__NR_utimes, __concretize_string(path), times);
+  if (r == -1)
+    errno = klee_get_errno();
+
+  return r;
+}
+
+
+int futimesat(int fd, const char* path, const struct timeval times[2]) {
+  if (fd != AT_FDCWD) {
+    exe_file_t *f = __get_file(fd);
+
+    if (!f) {
+      errno = EBADF;
+      return -1;
+    } else if (f->dfile) {
+      klee_warning("symbolic file descriptor, ignoring (ENOENT)");
+      errno = ENOENT;
+      return -1;
+    }
+    fd = f->fd;
+  }
+  if (__get_sym_file(path)) {
+    return utimes(path, times);
+  }
+
+  int r = syscall(__NR_futimesat, (long)fd,
+                 (path ? __concretize_string(path) : NULL),
+                 times);
+  if (r == -1)
+    errno = klee_get_errno();
+  return r;
+}
+ 
 int close(int fd) {
   static int n_calls = 0;
   exe_file_t *f;
@@ -446,6 +548,42 @@ int __fd_stat(const char *path, struct stat64 *buf) {
   }
 }
 
+int fstatat(int fd, const char *path, struct stat *buf, int flags) {  
+  if (fd != AT_FDCWD) {
+    exe_file_t *f = __get_file(fd);
+
+    if (!f) {
+      errno = EBADF;
+      return -1;
+    } else if (f->dfile) {
+      klee_warning("symbolic file descriptor, ignoring (ENOENT)");
+      errno = ENOENT;
+      return -1;
+    }
+    fd = f->fd;
+  }
+  exe_disk_file_t *dfile = __get_sym_file(path);
+  if (dfile) {
+    memcpy(buf, dfile->stat, sizeof(*dfile->stat));
+    return 0;
+  } 
+
+#if (defined __NR_newfstatat) && (__NR_newfstatat != 0)
+  int r = syscall(__NR_newfstatat, (long)fd,
+               (path ? __concretize_string(path) : NULL),
+               buf, (long)flags);
+#else
+  int r = syscall(__NR_fstatat64, (long)fd,
+               (path ? __concretize_string(path) : NULL),
+               buf, (long)flags);
+#endif
+
+  if (r == -1)
+    errno = klee_get_errno();
+  return r;
+}
+
+
 int __fd_lstat(const char *path, struct stat64 *buf) {
   exe_disk_file_t *dfile = __get_sym_file(path);
   if (dfile) {
@@ -1096,6 +1234,29 @@ int unlink(const char *pathname) {
   return -1;
 }
 
+int unlinkat(int dirfd, const char *pathname, int flags) {
+  /* similar to unlink. keep them separated though to avoid
+     problems if unlink changes to actually delete files */
+  exe_disk_file_t *dfile = __get_sym_file(pathname);
+  if (dfile) {
+    /* XXX check access */ 
+    if (S_ISREG(dfile->stat->st_mode)) {
+      dfile->stat->st_ino = 0;
+      return 0;
+    } else if (S_ISDIR(dfile->stat->st_mode)) {
+      errno = EISDIR;
+      return -1;
+    } else {
+      errno = EPERM;
+      return -1;
+    }
+  }
+
+  klee_warning("ignoring (EPERM)");
+  errno = EPERM;
+  return -1;
+}
+
 ssize_t readlink(const char *path, char *buf, size_t bufsize) {
   exe_disk_file_t *dfile = __get_sym_file(path);
   if (dfile) {
diff --git a/runtime/POSIX/fd.h b/runtime/POSIX/fd.h
index f2780143..cb86295c 100644
--- a/runtime/POSIX/fd.h
+++ b/runtime/POSIX/fd.h
@@ -79,6 +79,7 @@ void klee_init_env(int *argcPtr, char ***argvPtr);
 /* *** */
 
 int __fd_open(const char *pathname, int flags, mode_t mode);
+int __fd_openat(int basefd, const char *pathname, int flags, mode_t mode);
 off64_t __fd_lseek(int fd, off64_t offset, int whence);
 int __fd_stat(const char *path, struct stat64 *buf);
 int __fd_lstat(const char *path, struct stat64 *buf);
diff --git a/runtime/POSIX/fd_32.c b/runtime/POSIX/fd_32.c
index 1e96de37..389d7ae8 100644
--- a/runtime/POSIX/fd_32.c
+++ b/runtime/POSIX/fd_32.c
@@ -18,7 +18,7 @@
 #endif
 
 #include "klee/Config/Version.h"
-#if defined(ENV32) || (LLVM_VERSION_CODE < LLVM_VERSION(3, 3))
+#if defined(ENV32) || (LLVM_VERSION_CODE < LLVM_VERSION(3, 2))
 #define _LARGEFILE64_SOURCE
 #include "fd.h"
 
@@ -53,6 +53,12 @@ static void __stat64_to_stat(struct stat64 *a, struct stat *b) {
   b->st_ctime = a->st_ctime;
   b->st_blksize = a->st_blksize;
   b->st_blocks = a->st_blocks;
+#ifdef _BSD_SOURCE
+  b->st_atim.tv_nsec = a->st_atim.tv_nsec;
+  b->st_mtim.tv_nsec = a->st_mtim.tv_nsec;
+  b->st_ctim.tv_nsec = a->st_ctim.tv_nsec;
+#endif
+
 }
 
 /***/
@@ -71,6 +77,20 @@ int open(const char *pathname, int flags, ...) {
   return __fd_open(pathname, flags, mode);
 }
 
+int openat(int fd, const char *pathname, int flags, ...) {
+  mode_t mode = 0;
+
+  if (flags & O_CREAT) {
+    /* get mode */
+    va_list ap;
+    va_start(ap, flags);
+    mode = va_arg(ap, mode_t);
+    va_end(ap);
+  }
+
+  return __fd_openat(fd, pathname, flags, mode);
+}
+
 off_t lseek(int fd, off_t off, int whence) {
   return (off_t) __fd_lseek(fd, off, whence);
 }
diff --git a/runtime/POSIX/fd_64.c b/runtime/POSIX/fd_64.c
index 268579c0..21a986aa 100644
--- a/runtime/POSIX/fd_64.c
+++ b/runtime/POSIX/fd_64.c
@@ -17,7 +17,7 @@
 
 
 #include "klee/Config/Version.h"
-#if defined(ENV64) || (LLVM_VERSION_CODE < LLVM_VERSION(3, 3))
+#if defined(ENV64) || (LLVM_VERSION_CODE < LLVM_VERSION(3, 2))
 #define _LARGEFILE64_SOURCE
 #define _FILE_OFFSET_BITS 64
 #include "fd.h"
@@ -57,6 +57,20 @@ int open(const char *pathname, int flags, ...) {
   return __fd_open(pathname, flags, mode);
 }
 
+int openat(int fd, const char *pathname, int flags, ...) {
+  mode_t mode = 0;
+  
+  if (flags & O_CREAT) {
+    /* get mode */
+    va_list ap;
+    va_start(ap, flags);
+    mode = va_arg(ap, mode_t);
+    va_end(ap);
+  }
+
+  return __fd_openat(fd, pathname, flags, mode);
+}
+
 off64_t lseek(int fd, off64_t offset, int whence) {
   return __fd_lseek(fd, offset, whence);
 }
diff --git a/runtime/POSIX/stubs.c b/runtime/POSIX/stubs.c
index 3a9d380c..7a424d05 100644
--- a/runtime/POSIX/stubs.c
+++ b/runtime/POSIX/stubs.c
@@ -222,13 +222,6 @@ int utime(const char *filename, const struct utimbuf *buf) {
   return -1;
 }
 
-int utimes(const char *filename, const struct timeval times[2]) __attribute__((weak));
-int utimes(const char *filename, const struct timeval times[2]) {
-  klee_warning("ignoring (EPERM)");
-  errno = EPERM;
-  return -1;
-}
-
 int futimes(int fd, const struct timeval times[2]) __attribute__((weak));
 int futimes(int fd, const struct timeval times[2]) {
   klee_warning("ignoring (EBADF)");
diff --git a/test/Runtime/POSIX/Futimesat.c b/test/Runtime/POSIX/Futimesat.c
new file mode 100644
index 00000000..fd9ea0de
--- /dev/null
+++ b/test/Runtime/POSIX/Futimesat.c
@@ -0,0 +1,43 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -g -c -o %t2.bc
+// RUN: touch /tmp/futimesat-dummy
+// RUN: %klee --posix-runtime --exit-on-error %t2.bc --sym-files 1 10
+// RUN: rm /tmp/futimesat-dummy
+
+#include <assert.h>
+#include <fcntl.h>
+#include <sys/stat.h>
+#include <time.h>
+
+int main(int argc, char **argv) {
+  int r;
+  struct stat buf;
+  struct timeval times[2];
+
+  times[0].tv_sec = time(NULL)-3600;
+  times[0].tv_usec = 0;
+  times[1].tv_sec = time(NULL)-3600;
+  times[1].tv_usec = 0;
+
+  r = futimesat(AT_FDCWD, "A", times);
+  assert(r != -1);
+
+  r = fstatat(AT_FDCWD, "A", &buf, 0);
+  assert(r != -1);
+  assert(buf.st_atime == times[0].tv_sec &&
+         buf.st_mtime == times[1].tv_sec);
+
+  /* assumes /tmp exists and is writeable */
+  int fd = open("/tmp", O_RDONLY);
+  assert(fd > 0);
+  r = futimesat(fd, "futimesat-dummy", times);
+  assert(r != -1);
+
+  r = fstatat(fd, "futimesat-dummy", &buf, 0);
+  assert(r != -1);
+  assert(buf.st_atime == times[0].tv_sec &&
+         buf.st_mtime == times[1].tv_sec);
+
+  close(fd);
+
+  return 0;
+}
diff --git a/test/Runtime/POSIX/Openat.c b/test/Runtime/POSIX/Openat.c
new file mode 100644
index 00000000..d417ee47
--- /dev/null
+++ b/test/Runtime/POSIX/Openat.c
@@ -0,0 +1,18 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t2.bc
+// RUN: %klee --posix-runtime --exit-on-error %t2.bc --sym-files 1 10
+// RUN: test -f klee-last/test000001.ktest
+
+#include <assert.h>
+#include <fcntl.h>
+
+int main(int argc, char **argv) {
+  int fd = openat(AT_FDCWD, "A", O_RDWR|O_TRUNC);
+  if (fd != -1) {
+    char buf[10];
+    assert(read(fd, buf, 10) == 10);
+    assert(klee_is_symbolic(buf[0]));
+  } else {
+    klee_silent_exit(0);
+  }
+  return 0;
+}
diff --git a/tools/klee/Makefile b/tools/klee/Makefile
index 01486fef..e1dbefce 100644
--- a/tools/klee/Makefile
+++ b/tools/klee/Makefile
@@ -15,6 +15,9 @@ include $(LEVEL)/Makefile.config
 USEDLIBS = kleeCore.a kleeBasic.a kleeModule.a  kleaverSolver.a kleaverExpr.a kleeSupport.a 
 LINK_COMPONENTS = jit bitreader bitwriter ipo linker engine
 
+ifeq ($(shell echo "$(LLVM_VERSION_MAJOR).$(LLVM_VERSION_MINOR) >= 3.3" | bc), 1)
+LINK_COMPONENTS += irreader
+endif
 include $(LEVEL)/Makefile.common
 
 LIBS += -lstp
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-10-04 09:22:58 +0000