about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile.config.in1
-rw-r--r--Makefile.rules12
-rw-r--r--autoconf/configure.ac5
-rwxr-xr-xconfigure235
-rw-r--r--lib/Core/Executor.h2
-rw-r--r--lib/Module/IntrinsicCleaner.cpp10
-rw-r--r--test/Feature/OverflowMul.ll43
-rw-r--r--tools/klee/main.cpp10
8 files changed, 210 insertions, 108 deletions
diff --git a/Makefile.config.in b/Makefile.config.in
index c392136a..c916a456 100644
--- a/Makefile.config.in
+++ b/Makefile.config.in
@@ -51,3 +51,4 @@ CXXFLAGS := @CXXFLAGS@
 LDFLAGS := @LDFLAGS@
 
 REQUIRES_RTTI := @REQUIRES_RTTI@
+RUNTEST := @RUNTEST@
diff --git a/Makefile.rules b/Makefile.rules
index e5ce2b23..f01649a9 100644
--- a/Makefile.rules
+++ b/Makefile.rules
@@ -451,6 +451,13 @@ else
     LLVMCC := $(LLVMGCC)
     LLVMCXX := $(LLVMGXX)
   endif
+
+  ifeq ($(wildcard $(LLVMCC)),)
+    $(warning Provided Compiler "$(LLVMCC)" is not found. Provide full path!)
+  endif
+  ifeq ($(wildcard $(LLVMCXX)),)
+    $(warning Provided Compiler "$(LLVMCXX)" is not found. Provide full path!)
+  endif
 endif
 
 #--------------------------------------------------------------------
@@ -470,7 +477,7 @@ ifndef TBLGEN
 endif
 LLVM_CONFIG := $(LLVMToolDir)/llvm-config
 ifndef LLVMLD
-LLVMLD    := $(LLVMToolDir)/llvm-ld$(EXEEXT)
+LLVMLD    := $(LLVMToolDir)/llvm-link$(EXEEXT)
 endif
 ifndef LLVMDIS
 LLVMDIS  := $(LLVMToolDir)/llvm-dis$(EXEEXT)
@@ -1039,7 +1046,7 @@ $(warning Modules require LLVM capable compiler but none is available ****)
 else
 
 Module     := $(LibDir)/$(MODULE_NAME).bc
-LinkModule := $(LLVMLD) -r
+LinkModule := $(LLVMLD)
 
 
 ifdef EXPORTED_SYMBOL_FILE
@@ -1174,7 +1181,6 @@ ifdef BYTECODE_LIBRARY
 ifeq ($(strip $(LLVMCC)),)
 $(warning Bytecode libraries require LLVM capable compiler but none is available ****)
 else
-
 all-local:: $(LibName.BCA)
 
 ifdef EXPORTED_SYMBOL_FILE
diff --git a/autoconf/configure.ac b/autoconf/configure.ac
index c78dcb50..6d846d5d 100644
--- a/autoconf/configure.ac
+++ b/autoconf/configure.ac
@@ -348,6 +348,11 @@ else
 fi
 
 dnl **************************************************************************
+dnl * Check for dejagnu
+dnl **************************************************************************
+AC_PATH_PROG(RUNTEST, [runtest])
+
+dnl **************************************************************************
 dnl * Create the output files
 dnl **************************************************************************
 
diff --git a/configure b/configure
index dbdfe5b4..eb61b85b 100755
--- a/configure
+++ b/configure
@@ -1,11 +1,13 @@
 #! /bin/sh
 # Guess values for system-dependent variables and create Makefiles.
-# Generated by GNU Autoconf 2.69 for KLEE 0.01.
+# Generated by GNU Autoconf 2.68 for KLEE 0.01.
 #
 # Report bugs to <daniel@minormatter.com>.
 #
 #
-# Copyright (C) 1992-1996, 1998-2012 Free Software Foundation, Inc.
+# Copyright (C) 1992, 1993, 1994, 1995, 1996, 1998, 1999, 2000, 2001,
+# 2002, 2003, 2004, 2005, 2006, 2007, 2008, 2009, 2010 Free Software
+# Foundation, Inc.
 #
 #
 # This configure script is free software; the Free Software Foundation
@@ -134,31 +136,6 @@ export LANGUAGE
 # CDPATH.
 (unset CDPATH) >/dev/null 2>&1 && unset CDPATH
 
-# Use a proper internal environment variable to ensure we don't fall
-  # into an infinite loop, continuously re-executing ourselves.
-  if test x"${_as_can_reexec}" != xno && test "x$CONFIG_SHELL" != x; then
-    _as_can_reexec=no; export _as_can_reexec;
-    # 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
-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+"$@"}
-# Admittedly, this is quite paranoid, since all the known shells bail
-# out after a failed `exec'.
-$as_echo "$0: could not re-execute with $CONFIG_SHELL" >&2
-as_fn_exit 255
-  fi
-  # We don't want this to propagate to other subprocesses.
-          { _as_can_reexec=; unset _as_can_reexec;}
 if test "x$CONFIG_SHELL" = x; then
   as_bourne_compatible="if test -n \"\${ZSH_VERSION+set}\" && (emulate sh) >/dev/null 2>&1; then :
   emulate sh
@@ -192,8 +169,7 @@ if ( set x; as_fn_ret_success y && test x = \"\$1\" ); then :
 else
   exitcode=1; echo positional parameters were not saved.
 fi
-test x\$exitcode = x0 || exit 1
-test -x / || exit 1"
+test x\$exitcode = x0 || exit 1"
   as_suggested="  as_lineno_1=";as_suggested=$as_suggested$LINENO;as_suggested=$as_suggested" as_lineno_1a=\$LINENO
   as_lineno_2=";as_suggested=$as_suggested$LINENO;as_suggested=$as_suggested" as_lineno_2a=\$LINENO
   eval 'test \"x\$as_lineno_1'\$as_run'\" != \"x\$as_lineno_2'\$as_run'\" &&
@@ -238,25 +214,21 @@ IFS=$as_save_IFS
 
 
       if test "x$CONFIG_SHELL" != x; then :
-  export CONFIG_SHELL
-             # 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
-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+"$@"}
-# Admittedly, this is quite paranoid, since all the known shells bail
-# out after a failed `exec'.
-$as_echo "$0: could not re-execute with $CONFIG_SHELL" >&2
-exit 255
+  # 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+"$@"}
 fi
 
     if test x$as_have_required = xno; then :
@@ -359,14 +331,6 @@ $as_echo X"$as_dir" |
 
 
 } # as_fn_mkdir_p
-
-# as_fn_executable_p FILE
-# -----------------------
-# Test if FILE is an executable regular file.
-as_fn_executable_p ()
-{
-  test -f "$1" && test -x "$1"
-} # as_fn_executable_p
 # as_fn_append VAR VALUE
 # ----------------------
 # Append the text in VALUE to the end of the definition contained in VAR. Take
@@ -488,10 +452,6 @@ as_cr_alnum=$as_cr_Letters$as_cr_digits
   chmod +x "$as_me.lineno" ||
     { $as_echo "$as_me: error: cannot create $as_me.lineno; rerun with a POSIX shell" >&2; as_fn_exit 1; }
 
-  # If we had to re-execute with $CONFIG_SHELL, we're ensured to have
-  # already done that, so ensure we don't try to do so again and fall
-  # in an infinite loop.  This has already happened in practice.
-  _as_can_reexec=no; export _as_can_reexec
   # Don't try to exec as it changes $[0], causing all sort of problems
   # (the dirname of $[0] is not the place where we might find the
   # original and so on.  Autoconf is especially sensitive to this).
@@ -526,16 +486,16 @@ if (echo >conf$$.file) 2>/dev/null; then
     # ... but there are two gotchas:
     # 1) On MSYS, both `ln -s file dir' and `ln file dir' fail.
     # 2) DJGPP < 2.04 has no symlinks; `ln -s' creates a wrapper executable.
-    # In both cases, we have to default to `cp -pR'.
+    # In both cases, we have to default to `cp -p'.
     ln -s conf$$.file conf$$.dir 2>/dev/null && test ! -f conf$$.exe ||
-      as_ln_s='cp -pR'
+      as_ln_s='cp -p'
   elif ln conf$$.file conf$$ 2>/dev/null; then
     as_ln_s=ln
   else
-    as_ln_s='cp -pR'
+    as_ln_s='cp -p'
   fi
 else
-  as_ln_s='cp -pR'
+  as_ln_s='cp -p'
 fi
 rm -f conf$$ conf$$.exe conf$$.dir/conf$$.file conf$$.file
 rmdir conf$$.dir 2>/dev/null
@@ -547,8 +507,28 @@ else
   as_mkdir_p=false
 fi
 
-as_test_x='test -x'
-as_executable_p=as_fn_executable_p
+if test -x / >/dev/null 2>&1; then
+  as_test_x='test -x'
+else
+  if ls -dL / >/dev/null 2>&1; then
+    as_ls_L_option=L
+  else
+    as_ls_L_option=
+  fi
+  as_test_x='
+    eval sh -c '\''
+      if test -d "$1"; then
+	test -d "$1/.";
+      else
+	case $1 in #(
+	-*)set "./$1";;
+	esac;
+	case `ls -ld'$as_ls_L_option' "$1" 2>/dev/null` in #((
+	???[sx]*):;;*)false;;esac;fi
+    '\'' sh
+  '
+fi
+as_executable_p=$as_test_x
 
 # Sed expression to map a string onto a valid CPP name.
 as_tr_cpp="eval sed 'y%*$as_cr_letters%P$as_cr_LETTERS%;s%[^_$as_cr_alnum]%_%g'"
@@ -624,6 +604,7 @@ ac_includes_default="\
 
 ac_subst_vars='LTLIBOBJS
 LIBOBJS
+RUNTEST
 STP_ROOT
 CXXCPP
 ac_ct_CXX
@@ -1183,6 +1164,8 @@ target=$target_alias
 if test "x$host_alias" != x; then
   if test "x$build_alias" = x; then
     cross_compiling=maybe
+    $as_echo "$as_me: WARNING: if you wanted to set the --build type, don't use --host.
+    If a cross compiler is detected then cross compile mode will be used" >&2
   elif test "x$build_alias" != "x$host_alias"; then
     cross_compiling=yes
   fi
@@ -1437,9 +1420,9 @@ test -n "$ac_init_help" && exit $ac_status
 if $ac_init_version; then
   cat <<\_ACEOF
 KLEE configure 0.01
-generated by GNU Autoconf 2.69
+generated by GNU Autoconf 2.68
 
-Copyright (C) 2012 Free Software Foundation, Inc.
+Copyright (C) 2010 Free Software Foundation, Inc.
 This configure script is free software; the Free Software Foundation
 gives unlimited permission to copy, distribute and modify it.
 _ACEOF
@@ -1882,7 +1865,7 @@ $as_echo "$ac_try_echo"; } >&5
 	 test ! -s conftest.err
        } && test -s conftest$ac_exeext && {
 	 test "$cross_compiling" = yes ||
-	 test -x conftest$ac_exeext
+	 $as_test_x conftest$ac_exeext
        }; then :
   ac_retval=0
 else
@@ -1905,7 +1888,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.69.  Invocation command line was
+generated by GNU Autoconf 2.68.  Invocation command line was
 
   $ $0 $@
 
@@ -2796,7 +2779,7 @@ do
   IFS=$as_save_IFS
   test -z "$as_dir" && as_dir=.
     for ac_exec_ext in '' $ac_executable_extensions; do
-  if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then
+  if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then
     ac_cv_prog_CC="${ac_tool_prefix}gcc"
     $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
     break 2
@@ -2836,7 +2819,7 @@ do
   IFS=$as_save_IFS
   test -z "$as_dir" && as_dir=.
     for ac_exec_ext in '' $ac_executable_extensions; do
-  if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then
+  if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then
     ac_cv_prog_ac_ct_CC="gcc"
     $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
     break 2
@@ -2889,7 +2872,7 @@ do
   IFS=$as_save_IFS
   test -z "$as_dir" && as_dir=.
     for ac_exec_ext in '' $ac_executable_extensions; do
-  if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then
+  if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then
     ac_cv_prog_CC="${ac_tool_prefix}cc"
     $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
     break 2
@@ -2930,7 +2913,7 @@ do
   IFS=$as_save_IFS
   test -z "$as_dir" && as_dir=.
     for ac_exec_ext in '' $ac_executable_extensions; do
-  if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then
+  if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then
     if test "$as_dir/$ac_word$ac_exec_ext" = "/usr/ucb/cc"; then
        ac_prog_rejected=yes
        continue
@@ -2988,7 +2971,7 @@ do
   IFS=$as_save_IFS
   test -z "$as_dir" && as_dir=.
     for ac_exec_ext in '' $ac_executable_extensions; do
-  if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then
+  if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then
     ac_cv_prog_CC="$ac_tool_prefix$ac_prog"
     $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
     break 2
@@ -3032,7 +3015,7 @@ do
   IFS=$as_save_IFS
   test -z "$as_dir" && as_dir=.
     for ac_exec_ext in '' $ac_executable_extensions; do
-  if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then
+  if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then
     ac_cv_prog_ac_ct_CC="$ac_prog"
     $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
     break 2
@@ -3478,7 +3461,8 @@ cat confdefs.h - <<_ACEOF >conftest.$ac_ext
 /* end confdefs.h.  */
 #include <stdarg.h>
 #include <stdio.h>
-struct stat;
+#include <sys/types.h>
+#include <sys/stat.h>
 /* Most of the following tests are stolen from RCS 5.7's src/conf.sh.  */
 struct buf { int x; };
 FILE * (*rcsopen) (struct buf *, struct stat *, int);
@@ -3718,7 +3702,7 @@ do
     for ac_prog in grep ggrep; do
     for ac_exec_ext in '' $ac_executable_extensions; do
       ac_path_GREP="$as_dir/$ac_prog$ac_exec_ext"
-      as_fn_executable_p "$ac_path_GREP" || continue
+      { test -f "$ac_path_GREP" && $as_test_x "$ac_path_GREP"; } || continue
 # Check for GNU ac_path_GREP and select it if it is found.
   # Check for GNU $ac_path_GREP
 case `"$ac_path_GREP" --version 2>&1` in
@@ -3784,7 +3768,7 @@ do
     for ac_prog in egrep; do
     for ac_exec_ext in '' $ac_executable_extensions; do
       ac_path_EGREP="$as_dir/$ac_prog$ac_exec_ext"
-      as_fn_executable_p "$ac_path_EGREP" || continue
+      { test -f "$ac_path_EGREP" && $as_test_x "$ac_path_EGREP"; } || continue
 # Check for GNU ac_path_EGREP and select it if it is found.
   # Check for GNU $ac_path_EGREP
 case `"$ac_path_EGREP" --version 2>&1` in
@@ -4009,7 +3993,7 @@ do
   IFS=$as_save_IFS
   test -z "$as_dir" && as_dir=.
     for ac_exec_ext in '' $ac_executable_extensions; do
-  if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then
+  if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then
     ac_cv_prog_CXX="$ac_tool_prefix$ac_prog"
     $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
     break 2
@@ -4053,7 +4037,7 @@ do
   IFS=$as_save_IFS
   test -z "$as_dir" && as_dir=.
     for ac_exec_ext in '' $ac_executable_extensions; do
-  if as_fn_executable_p "$as_dir/$ac_word$ac_exec_ext"; then
+  if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then
     ac_cv_prog_ac_ct_CXX="$ac_prog"
     $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
     break 2
@@ -4480,6 +4464,47 @@ fi
 
 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 :
+  $as_echo_n "(cached) " >&6
+else
+  case $RUNTEST in
+  [\\/]* | ?:[\\/]*)
+  ac_cv_path_RUNTEST="$RUNTEST" # Let the user override the test with a path.
+  ;;
+  *)
+  as_save_IFS=$IFS; IFS=$PATH_SEPARATOR
+for as_dir in $PATH
+do
+  IFS=$as_save_IFS
+  test -z "$as_dir" && as_dir=.
+    for ac_exec_ext in '' $ac_executable_extensions; do
+  if { test -f "$as_dir/$ac_word$ac_exec_ext" && $as_test_x "$as_dir/$ac_word$ac_exec_ext"; }; then
+    ac_cv_path_RUNTEST="$as_dir/$ac_word$ac_exec_ext"
+    $as_echo "$as_me:${as_lineno-$LINENO}: found $as_dir/$ac_word$ac_exec_ext" >&5
+    break 2
+  fi
+done
+  done
+IFS=$as_save_IFS
+
+  ;;
+esac
+fi
+RUNTEST=$ac_cv_path_RUNTEST
+if test -n "$RUNTEST"; then
+  { $as_echo "$as_me:${as_lineno-$LINENO}: result: $RUNTEST" >&5
+$as_echo "$RUNTEST" >&6; }
+else
+  { $as_echo "$as_me:${as_lineno-$LINENO}: result: no" >&5
+$as_echo "no" >&6; }
+fi
+
+
+
 
 ac_config_commands="$ac_config_commands Makefile"
 
@@ -4913,16 +4938,16 @@ if (echo >conf$$.file) 2>/dev/null; then
     # ... but there are two gotchas:
     # 1) On MSYS, both `ln -s file dir' and `ln file dir' fail.
     # 2) DJGPP < 2.04 has no symlinks; `ln -s' creates a wrapper executable.
-    # In both cases, we have to default to `cp -pR'.
+    # In both cases, we have to default to `cp -p'.
     ln -s conf$$.file conf$$.dir 2>/dev/null && test ! -f conf$$.exe ||
-      as_ln_s='cp -pR'
+      as_ln_s='cp -p'
   elif ln conf$$.file conf$$ 2>/dev/null; then
     as_ln_s=ln
   else
-    as_ln_s='cp -pR'
+    as_ln_s='cp -p'
   fi
 else
-  as_ln_s='cp -pR'
+  as_ln_s='cp -p'
 fi
 rm -f conf$$ conf$$.exe conf$$.dir/conf$$.file conf$$.file
 rmdir conf$$.dir 2>/dev/null
@@ -4982,16 +5007,28 @@ else
   as_mkdir_p=false
 fi
 
-
-# as_fn_executable_p FILE
-# -----------------------
-# Test if FILE is an executable regular file.
-as_fn_executable_p ()
-{
-  test -f "$1" && test -x "$1"
-} # as_fn_executable_p
-as_test_x='test -x'
-as_executable_p=as_fn_executable_p
+if test -x / >/dev/null 2>&1; then
+  as_test_x='test -x'
+else
+  if ls -dL / >/dev/null 2>&1; then
+    as_ls_L_option=L
+  else
+    as_ls_L_option=
+  fi
+  as_test_x='
+    eval sh -c '\''
+      if test -d "$1"; then
+	test -d "$1/.";
+      else
+	case $1 in #(
+	-*)set "./$1";;
+	esac;
+	case `ls -ld'$as_ls_L_option' "$1" 2>/dev/null` in #((
+	???[sx]*):;;*)false;;esac;fi
+    '\'' sh
+  '
+fi
+as_executable_p=$as_test_x
 
 # Sed expression to map a string onto a valid CPP name.
 as_tr_cpp="eval sed 'y%*$as_cr_letters%P$as_cr_LETTERS%;s%[^_$as_cr_alnum]%_%g'"
@@ -5013,7 +5050,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.69.  Invocation command line was
+generated by GNU Autoconf 2.68.  Invocation command line was
 
   CONFIG_FILES    = $CONFIG_FILES
   CONFIG_HEADERS  = $CONFIG_HEADERS
@@ -5079,10 +5116,10 @@ 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.69,
+configured by $0, generated by GNU Autoconf 2.68,
   with options \\"\$ac_cs_config\\"
 
-Copyright (C) 2012 Free Software Foundation, Inc.
+Copyright (C) 2010 Free Software Foundation, Inc.
 This config.status script is free software; the Free Software Foundation
 gives unlimited permission to copy, distribute and modify it."
 
@@ -5170,7 +5207,7 @@ fi
 _ACEOF
 cat >>$CONFIG_STATUS <<_ACEOF || ac_write_fail=1
 if \$ac_cs_recheck; then
-  set X $SHELL '$0' $ac_configure_args \$ac_configure_extra_args --no-create --no-recursion
+  set X '$SHELL' '$0' $ac_configure_args \$ac_configure_extra_args --no-create --no-recursion
   shift
   \$as_echo "running CONFIG_SHELL=$SHELL \$*" >&6
   CONFIG_SHELL='$SHELL'
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index a9d6b791..b7318a2c 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -287,7 +287,7 @@ private:
 
   /// Add the given (boolean) condition as a constraint on state. This
   /// function is a wrapper around the state's addConstraint function
-  /// which also manages manages propogation of implied values,
+  /// which also manages propagation of implied values,
   /// validity checks, and seed patching.
   void addConstraint(ExecutionState &state, ref<Expr> condition);
 
diff --git a/lib/Module/IntrinsicCleaner.cpp b/lib/Module/IntrinsicCleaner.cpp
index b897fcc7..2f18c17e 100644
--- a/lib/Module/IntrinsicCleaner.cpp
+++ b/lib/Module/IntrinsicCleaner.cpp
@@ -107,7 +107,8 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b) {
         break;
       }
 
-      case Intrinsic::uadd_with_overflow: {
+      case Intrinsic::uadd_with_overflow:
+      case Intrinsic::umul_with_overflow: {
         IRBuilder<> builder(ii->getParent(), ii);
 
 #if LLVM_VERSION_CODE < LLVM_VERSION(2, 8)
@@ -118,7 +119,12 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b) {
         Value *op2 = ii->getArgOperand(1);
 #endif
         
-        Value *result = builder.CreateAdd(op1, op2);
+        Value *result = 0;
+        if (ii->getIntrinsicID() == Intrinsic::uadd_with_overflow)
+          result = builder.CreateAdd(op1, op2);
+        else
+          result = builder.CreateMul(op1, op2);
+
         Value *overflow = builder.CreateICmpULT(result, op1);
         
         Value *resultStruct =
diff --git a/test/Feature/OverflowMul.ll b/test/Feature/OverflowMul.ll
new file mode 100644
index 00000000..7ab67502
--- /dev/null
+++ b/test/Feature/OverflowMul.ll
@@ -0,0 +1,43 @@
+; RUN: llvm-as %s -f -o %t1.bc
+; RUN: %klee -disable-opt %t1.bc > %t2
+; RUN: grep PASS %t2
+
+target datalayout = "e-p:64:64:64-i1:8:8-i8:8:8-i16:16:16-i32:32:32-i64:64:64-f32:32:32-f64:64:64-v64:64:64-v128:128:128-a0:0:64-s0:64:64-f80:128:128-n8:16:32:64"
+target triple = "x86_64-unknown-linux-gnu"
+
+declare {i8, i1} @llvm.umul.with.overflow.i8(i8 %a, i8 %b)
+
+declare i32 @puts(i8*)
+
+@.passstr = private constant [5 x i8] c"PASS\00", align 1
+@.failstr = private constant [5 x i8] c"FAIL\00", align 1
+
+define i32 @main() {
+bb0:
+  %s0 = call {i8, i1} @llvm.umul.with.overflow.i8(i8 1, i8 128)
+  %v0 = extractvalue {i8, i1} %s0, 0
+  %c0 = icmp eq i8 %v0, 128
+  br i1 %c0, label %bb0_1, label %bbfalse
+
+bb0_1:
+  %o0 = extractvalue {i8, i1} %s0, 1
+  br i1 %o0, label %bbfalse, label %bb1
+
+bb1:
+  %s1 = call {i8, i1} @llvm.umul.with.overflow.i8(i8 2, i8 128)
+  %v1 = extractvalue {i8, i1} %s1, 0
+  %c1 = icmp eq i8 %v1, 0
+  br i1 %c1, label %bb1_1, label %bbfalse
+
+bb1_1:
+  %o1 = extractvalue {i8, i1} %s1, 1
+  br i1 %o1, label %bbtrue, label %bbfalse
+  
+bbtrue:
+  %0 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.passstr, i64 0, i64 0)) nounwind
+  ret i32 0
+
+bbfalse:
+  %1 = call i32 @puts(i8* getelementptr inbounds ([5 x i8]* @.failstr, i64 0, i64 0)) nounwind
+  ret i32 0
+}
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index 0c485571..79f29d2d 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -670,8 +670,8 @@ static int initEnv(Module *mainModule) {
 }
 
 
-// This is a terrible hack until we get some real modelling of the
-// system. All we do is check the undefined symbols and m and warn about
+// This is a terrible hack until we get some real modeling of the
+// system. All we do is check the undefined symbols and warn about
 // any "unrecognized" externals and about any obviously unsafe ones.
 
 // Symbols we explicitly support
@@ -715,7 +715,11 @@ static const char *modelledExternals[] = {
   "klee_warning_once", 
   "klee_alias_function",
   "klee_stack_trace",
-  "llvm.dbg.stoppoint", 
+  "llvm.dbg.stoppoint",
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 1)
+  "llvm.dbg.declare",
+  "llvm.dbg.value",
+#endif
   "llvm.va_start", 
   "llvm.va_end", 
   "malloc",
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-04-06 18:26:36 +0000