about summary refs log tree commit diff homepage
path: root/autoconf/configure.ac
blob: c6e59d974b39c44d2dd1f03e5afafffcba21902a (plain) (blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
dnl **************************************************************************
dnl * Initialize
dnl **************************************************************************
AC_INIT([[KLEE]],[[0.01]],[daniel@minormatter.com])

dnl Identify where LLVM source tree is (this is patched by
dnl AutoRegen.sh)
LLVM_SRC_ROOT=XXX

dnl Tell autoconf that the auxilliary files are actually located in
dnl the LLVM autoconf directory, not here.
AC_CONFIG_AUX_DIR($LLVM_SRC_ROOT/autoconf)

dnl Tell autoconf that this is an LLVM project being configured
dnl This provides the --with-llvmsrc and --with-llvmobj options
LLVM_CONFIG_PROJECT("","")

dnl Verify that the source directory is valid
AC_CONFIG_SRCDIR(["Makefile.config.in"])

dnl Configure a common Makefile
AC_CONFIG_FILES(Makefile.config)

dnl Configure Doxygen file
AC_CONFIG_FILES([docs/doxygen.cfg])

dnl Configure project makefiles
dnl List every Makefile that exists within your source tree
AC_CONFIG_HEADERS([include/klee/Config/config.h])

AH_TOP([#ifndef KLEE_CONFIG_CONFIG_H
#define KLEE_CONFIG_CONFIG_H])
AH_BOTTOM([#endif])

dnl FIXME: Make out of tree builds work.

AC_LANG([C++])

dnl **************************************************************************
dnl Find the host

AC_CANONICAL_TARGET

dnl Determine the platform type and cache its value. This helps us configure
dnl the System library to the correct build platform.
AC_CACHE_CHECK([type of operating system we're going to host on],
               [klee_cv_os_type],
[case $host in
  *-*-linux*)
    host_supports_posix_runtime=yes ;;
  *)
    host_supports_posix_runtime=no ;;
esac])

dnl **************************************************************************
dnl Verify that we can find llvm

dnl --with-llvm is a shortcut for setting srcdir and objdir.
AC_ARG_WITH(llvm,
  AS_HELP_STRING([--with-llvm],
    [Location of LLVM Source and Object code]),,)

AC_MSG_CHECKING([llvm source dir])

if test X${with_llvm} != X; then
    dnl Verify that --with-llvm{src,obj} were not given.
    if test X${with_llvmsrc} != X; then
       AC_MSG_ERROR([--with-llvmsrc cannot be specified when using --with-llvm])
    fi   
    if test X${with_llvmobj} != X; then
       AC_MSG_ERROR([--with-llvmobj cannot be specified when using --with-llvm])
    fi   
    with_llvmsrc=$with_llvm
    with_llvmobj=$with_llvm
fi

dnl If one of with_llvmsrc or with_llvmobj was given, we must have both.
if (test X${with_llvmsrc} != X || test X${with_llvmobj} != X); then
    dnl Verify that with_llvmobj was given as well.
    if test X${with_llvmsrc} = X; then
       AC_MSG_ERROR([--with-llvmsrc must be specified when using --with-llvmobj])
    fi      
    if test X${with_llvmobj} = X; then
       AC_MSG_ERROR([--with-llvmobj must be specified when using --with-llvmsrc])
    fi      
else
    dnl Otherwise try and use llvm-config to find.
    llvm_version=`llvm-config --version`
    if test X${llvm_version} = X; then
       AC_MSG_ERROR([unable to find llvm, use --with-llvmsrc and --with-llvmobj])
    fi
    
    with_llvmsrc=`llvm-config --src-root`
    with_llvmobj=`llvm-config --obj-root`
fi

dnl Try to validate directories.
if test ! -f ${with_llvmsrc}/Makefile.rules; then
   AC_MSG_ERROR([invalid llvmsrc directory: ${with_llvmsrc}])
fi
if test ! -f ${with_llvmobj}/Makefile.config; then
   AC_MSG_ERROR([invalid llvmobj directory: ${with_llvmobj}])
fi

dnl Make the paths absolute.
llvm_src=`cd $with_llvmsrc 2> /dev/null; pwd`
llvm_obj=`cd $with_llvmobj 2> /dev/null; pwd`
   
AC_MSG_RESULT([$llvm_src])

dnl Report obj dir as well.
AC_MSG_CHECKING([llvm obj dir])
AC_MSG_RESULT([$llvm_obj])

AC_SUBST(LLVM_SRC,$llvm_src)
AC_SUBST(LLVM_OBJ,$llvm_obj)

dnl Determine LLVM version.
AC_MSG_CHECKING([llvm package version])
llvm_package_version=`grep PACKAGE_VERSION= $with_llvmsrc/configure | cut -d\' -f 2`
AC_MSG_RESULT([$llvm_package_version])

llvm_version_split=`python -c "import re; print('\t'.join(map(str, re.match('([[0-9]]+)[.]([[0-9]]+)(svn)?', \"$llvm_package_version\").groups())))"`

AC_MSG_CHECKING([llvm version major])
llvm_version_major=`echo "$llvm_version_split" | cut -f 1`
AC_MSG_RESULT([$llvm_version_major])

AC_MSG_CHECKING([llvm version minor])
llvm_version_minor=`echo "$llvm_version_split" | cut -f 2`
AC_MSG_RESULT([$llvm_version_minor])

AC_MSG_CHECKING([llvm is release version])
llvm_version_svn=`echo "$llvm_version_split" | cut -f 3`
if test "$llvm_version_svn" == "svn"; then
  llvm_is_release=0
else
  llvm_is_release=1
fi
AC_MSG_RESULT([$llvm_is_release])

AC_DEFINE_UNQUOTED(LLVM_VERSION_MAJOR, $llvm_version_major, [LLVM major version number])
AC_SUBST(LLVM_VERSION_MAJOR,$llvm_version_major)
AC_DEFINE_UNQUOTED(LLVM_VERSION_MINOR, $llvm_version_minor, [LLVM minor version number])
AC_SUBST(LLVM_VERSION_MINOR,$llvm_version_minor)
AC_DEFINE_UNQUOTED(LLVM_IS_RELEASE, $llvm_is_release, [LLVM version is release (instead of development)])
AC_SUBST(LLVM_IS_RELEASE,$llvm_is_release)

dnl LLVM <= 2.6 requires RTTI.
if test $llvm_version_major -eq 2 -a $llvm_version_minor -le 6 ; then
  requires_rtti=1
else
  requires_rtti=0
fi
AC_SUBST(REQUIRES_RTTI,$requires_rtti)

AC_ARG_WITH(llvm-build-mode,
  AS_HELP_STRING([--with-llvm-build-mode],
    [LLVM build mode (e.g. Debug or Release, default autodetect)]),,[with_llvm_build_mode=check])

AC_MSG_CHECKING([llvm build mode])

if test X${with_llvm_build_mode} = Xcheck ; then
  llvm_configs="`ls -1 $llvm_obj/*/bin/llvm-config 2>/dev/null | head -n 1`"
  if test -x "$llvm_configs" ; then
    llvm_build_mode="`$llvm_configs --build-mode`"
  else
    AC_MSG_ERROR([Could not autodetect build mode])
  fi
else
  llvm_configs="`echo $llvm_obj/*/bin/llvm-config`"
  if test -x "$llvm_obj/$with_llvm_build_mode/bin/llvm-config" ; then
    llvm_build_mode=$with_llvm_build_mode
  else
    AC_MSG_ERROR([Invalid build mode: $llvm_build_mode])
  fi
fi

AC_MSG_RESULT([$llvm_build_mode])
AC_SUBST(LLVM_BUILD_MODE,$llvm_build_mode)

dnl **************************************************************************
dnl Detect a LLVM Bitcode compiler for building KLEE runtime library

dnl Check for clang built with llvm build
AC_MSG_CHECKING([LLVM Bitcode compiler])
klee_llvm_bc_c_compiler=""
klee_llvm_bc_cxx_compiler=""

AC_ARG_WITH([llvmcc],
            AS_HELP_STRING([--with-llvmcc],
                           [Set the path to the C LLVM bitcode compiler to use (Default: auto-detect). If set, --with-llvmcxx= must be set too.]
                          ),
            [],
            [with_llvmcc=none]
           )

AC_ARG_WITH([llvmcxx],
            AS_HELP_STRING([--with-llvmcxx],
                           [Set the path to the C++ LLVM bitcode compiler to use (Default: auto-detect). If set, --with-llvmcc= must be set too.]
                          ),
            [],
            [with_llvmcxx=none]
           )
if test \( "X$with_llvmcc" != Xnone -a "X$with_llvmcxx" = Xnone \) -o \( "X$with_llvmcxx" != Xnone -a "X$with_llvmcc" = Xnone \) ; then
    AC_MSG_ERROR([You must set both --with-llvmcc= and --with-llvmcxx= or set neither])
fi

if test X$with_llvmcc = Xnone ; then
    dnl Try to automatically find compiler
    
    dnl Try Clang inside the LLVM build
    if test -x "$llvm_obj/$llvm_build_mode/bin/clang" ; then
        AC_MSG_RESULT([Found clang in LLVM Build])
        klee_llvm_bc_c_compiler="$llvm_obj/$llvm_build_mode/bin/clang"

        if test -x "$llvm_obj/$llvm_build_mode/bin/clang++" ; then
            klee_llvm_bc_cxx_compiler="$llvm_obj/$llvm_build_mode/bin/clang++"
        else
            AC_MSG_ERROR([Found clang but could not find clang++])
        fi
    fi

    dnl Try llvm-gcc in PATH
    if test "X${klee_llvm_bc_c_compiler}" = X ; then
        AC_MSG_RESULT([]) # Force a new line
        AC_CHECK_PROG(llvm_gcc,llvm-gcc,FOUND,NOT_FOUND)
        if test ${llvm_gcc} = FOUND ; then
            klee_llvm_bc_c_compiler=`which llvm-gcc`

            AC_CHECK_PROG(llvm_gxx,llvm-g++,FOUND,NOT_FOUND)
            if test ${llvm_gxx} = FOUND; then
                klee_llvm_bc_cxx_compiler=`which llvm-g++`
            else
                AC_MSG_ERROR([Found llvm-gcc but could not find llvm-g++ in PATH])
            fi
        fi

    fi

    dnl Try clang in PATH
    if test "X${klee_llvm_bc_c_compiler}" = X ; then
        AC_MSG_RESULT([]) # Force a new line
        AC_CHECK_PROG(clang,clang,FOUND,NOT_FOUND)
        if test ${clang} = FOUND ; then
            klee_llvm_bc_c_compiler=`which clang`

            AC_CHECK_PROG(clang_cxx,clang++,FOUND,NOT_FOUND)
            if test ${clang_cxx} = FOUND; then
                klee_llvm_bc_cxx_compiler=`which clang++`
            else
                AC_MSG_ERROR([Found clang but could not find clang++ in PATH])
            fi
        fi

    fi

    if test X"${klee_llvm_bc_c_compiler}" = X ; then
        AC_MSG_ERROR([Could not find a C LLVM Bitcode compiler. Did you try building Clang in the LLVM Build directory or putting llvm-gcc or clang in your path?])
    fi

    if test X"${klee_llvm_bc_cxx_compiler}" = X ; then
        AC_MSG_ERROR([Could not find a C++ LLVM Bitcode compiler. Did you try building Clang in the LLVM Build directory or putting llvm-gcc or clang in your path?])
    fi

else
    dnl Use user supplied values
    klee_llvm_bc_c_compiler="$with_llvmcc"
    klee_llvm_bc_cxx_compiler="$with_llvmcxx"

    if test \! -x "${klee_llvm_bc_c_compiler}"; then
        AC_MSG_ERROR([--with-llvmcc= supplied compiler does not exist])
    fi

    if test \! -x "${klee_llvm_bc_cxx_compiler}"; then
        AC_MSG_ERROR([--with-llvmcxx= supplied compiler does not exist])
    fi
    AC_MSG_RESULT([Using user supplied LLVM bitcode compilers.])
fi

dnl Tell the user what we are going to try and use
AC_MSG_RESULT([Using C llvm compiler : $klee_llvm_bc_c_compiler])
AC_MSG_RESULT([Using C++ llvm compiler : $klee_llvm_bc_cxx_compiler])

dnl Test that the bitcode compiler works

dnl Function for checking bitcode compiler works
dnl $1 : compiler to invoke
dnl $2 : source code extension (e.g. cpp or c)
dnl $3 : Compiler string (e.g. CXX or C)
function klee_check_bc()
{
    AC_MSG_CHECKING([${3} LLVM Bitcode compiler works])
    dnl FIXME: write to tmp directory instead of binary build dir
    klee_bc_test_file="./.klee_llvm_bitcode_test.${2}"

    echo "int main() { return 0;}" > "${klee_bc_test_file}"
    "${1}" -emit-llvm -c "${klee_bc_test_file}" -o "${klee_bc_test_file}.bc"
    if test $? -ne 0 ; then
        AC_MSG_ERROR([Failed running ${3} LLVM Bitcode compiler])
    fi

    if test \! -e "${klee_bc_test_file}.bc"; then
        AC_MSG_ERROR([ ${3} LLVM Bitcode compiler did not produce any output])
    fi

    dnl Convert bitcode to human readable form as a hacky check
    dnl that the version of LLVM we are configuring with can
    dnl parse the LLVM bitcode produced by the detected compiler
    if test -x "$llvm_obj/$llvm_build_mode/bin/llvm-dis" ; then
        "$llvm_obj/$llvm_build_mode/bin/llvm-dis" -o "${klee_bc_test_file}.ll" "${klee_bc_test_file}.bc"

        if test $? -ne 0; then
            AC_MSG_ERROR([Failed converting LLVM Bitcode to LLVM assembly. Maybe your LLVM versions do not match?])
        fi

        if test -e "${klee_bc_test_file}.ll" ; then
            AC_MSG_RESULT([Success])
            rm "${klee_bc_test_file}" "${klee_bc_test_file}.bc" "${klee_bc_test_file}.ll"
        else
            rm "${klee_bc_test_file}" "${klee_bc_test_file}.bc" "${klee_bc_test_file}.ll"
            AC_MSG_ERROR([Failed converting LLVM Bitcode to LLVM assembly. Maybe your LLVM versions do not match?])
        fi
        
    else
        rm "${klee_bc_test_file}" "${klee_bc_test_file}.bc"
        AC_MSG_ERROR([Could not find llvm-dis])
    fi
}

dnl Invoke previously defined function to check the LLVM bitcode compilers
klee_check_bc "${klee_llvm_bc_c_compiler}" "c" "C"
klee_check_bc "${klee_llvm_bc_cxx_compiler}" "cpp" "CXX"

dnl Set variable for Makefile.config
AC_SUBST(KLEE_BITCODE_C_COMPILER,$klee_llvm_bc_c_compiler)
AC_SUBST(KLEE_BITCODE_CXX_COMPILER,$klee_llvm_bc_cxx_compiler)

dnl **************************************************************************
dnl User option to enable uClibc support.

AC_ARG_WITH(uclibc,
  AS_HELP_STRING([--with-uclibc],
                 [Enable use of the klee uclibc at the given path (klee-uclibc root directory or libc.a file]),,)

dnl Validate uclibc if given.

AC_MSG_CHECKING([uclibc])
if (test X${with_uclibc} != X); then
   if test  -d ${with_uclibc}; then
      dnl Support the legacy way of configuring with 
      dnl klee-uclibc, i.e. the root klee-uclibc
      dnl directory is passed as an argument.

      dnl Make the path absolute
      with_uclibc=`cd $with_uclibc 2> /dev/null; pwd`

      dnl create path to libc file
      KLEE_UCLIBC_BCA="${with_uclibc}/lib/libc.a"

      if test ! -e "${KLEE_UCLIBC_BCA}"; then
      AC_MSG_ERROR([Could not find file ${KLEE_UCLIBC_BCA}])
      fi
   elif test -f ${with_uclibc}; then
      dnl Support the new way of configuring klee-uclibc
      dnl i.e. the built bitcode archive is passed as the
      dnl argument.

      dnl Get absolute path to file
      _kud=`dirname ${with_uclibc}`
      _kud=`cd ${_kud}; pwd 2> /dev/null`
      _kuf=`basename ${with_uclibc}`

      KLEE_UCLIBC_BCA="${_kud}/${_kuf}" 
   else
      AC_MSG_ERROR([Could not detect klee-uclibc])
   fi

   dnl FIXME: Validate the libc.a file

   AC_MSG_RESULT([$KLEE_UCLIBC_BCA])
   AC_SUBST(ENABLE_UCLIBC,[[1]])
   AC_SUBST(KLEE_UCLIBC_BCA)
   AC_DEFINE(SUPPORT_KLEE_UCLIBC, [[1]], [klee-uclibc is supported])
else
   AC_MSG_RESULT([no])
   AC_SUBST(ENABLE_UCLIBC,[[0]])
fi


dnl **************************************************************************
dnl User option to enable the POSIX runtime

AC_ARG_ENABLE(posix-runtime,
              AS_HELP_STRING([--enable-posix-runtime],
                             [Enable the POSIX runtime]),
                             ,enableval=default)

AC_MSG_CHECKING([POSIX runtime])
if test ${enableval} = "default" ; then
  if test X${with_uclibc} != X; then
    enableval=$host_supports_posix_runtime
    if test ${enableval} = "yes"; then
      AC_MSG_RESULT([default (enabled)])
    else
      AC_MSG_RESULT([default (disabled, unsupported target)])
    fi
  else
    enableval="no"
    AC_MSG_RESULT([default (disabled, no uclibc)])
  fi
else
  if test ${enableval} = "yes" ; then
    AC_MSG_RESULT([yes])
  else
    AC_MSG_RESULT([no])
  fi
fi

if test ${enableval} = "yes" ; then
  AC_SUBST(ENABLE_POSIX_RUNTIME,[[1]])
else
  AC_SUBST(ENABLE_POSIX_RUNTIME,[[0]])
fi

dnl **************************************************************************
dnl User option to select runtime version

AC_ARG_WITH(runtime,
  AS_HELP_STRING([--with-runtime],
    [Select build configuration for runtime libraries (default [Release+Asserts])]),,
    withval=default)
if test X"${withval}" = Xdefault; then
   with_runtime=Release+Asserts
fi

AC_MSG_CHECKING([runtime configuration])
if test X${with_runtime} = XRelease; then
    AC_MSG_RESULT([Release])
    AC_SUBST(RUNTIME_ENABLE_OPTIMIZED,[[1]])
    AC_SUBST(RUNTIME_DISABLE_ASSERTIONS,[[1]])
    AC_SUBST(RUNTIME_DEBUG_SYMBOLS,[[]])
elif test X${with_runtime} = XRelease+Asserts; then
    AC_MSG_RESULT([Release+Asserts])
    AC_SUBST(RUNTIME_ENABLE_OPTIMIZED,[[1]])
    AC_SUBST(RUNTIME_DISABLE_ASSERTIONS,[[0]])
    AC_SUBST(RUNTIME_DEBUG_SYMBOLS,[[]])
elif test X${with_runtime} = XDebug; then
   AC_MSG_RESULT([Debug])
   AC_SUBST(RUNTIME_ENABLE_OPTIMIZED,[[0]])
   AC_SUBST(RUNTIME_DISABLE_ASSERTIONS,[[1]])
   AC_SUBST(RUNTIME_DEBUG_SYMBOLS,[[1]])
elif test X${with_runtime} = XDebug+Asserts; then
   AC_MSG_RESULT([Debug+Asserts])
   AC_SUBST(RUNTIME_ENABLE_OPTIMIZED,[[0]])
   AC_SUBST(RUNTIME_DISABLE_ASSERTIONS,[[0]])
   AC_SUBST(RUNTIME_DEBUG_SYMBOLS,[[1]])
else
   AC_MSG_ERROR([invalid configuration: ${with_runtime}])
fi

AC_DEFINE_UNQUOTED(RUNTIME_CONFIGURATION, "$with_runtime", [Configuration for runtime libraries])
AC_SUBST(RUNTIME_CONFIGURATION)

dnl **************************************************************************
dnl See if we should support __ctype_b_loc externals.

dnl FIXME: Do the proper test if we continue to need this.
case $host in
  *-*-linux*)
    AC_DEFINE_UNQUOTED(HAVE_CTYPE_EXTERNALS, 1, [Does the platform use __ctype_b_loc, etc.])
esac

dnl **************************************************************************
dnl Checks for header files.

dnl NOTE: This is mostly just to force autoconf to make CFLAGS defines
dnl for us.
AC_LANG_PUSH([C])

AC_CHECK_HEADERS([sys/acl.h])

AC_CHECK_LIB([cap], [cap_get_proc], [have_cap=yes], [have_cap=no])
if test "x${have_cap}" = xyes; then
  AC_CHECK_HEADERS([sys/capability.h], [], [have_cap=no])
fi
if test "x${have_cap}" = xno; then
  AC_MSG_WARN([Library cap and its header file sys/capability.h not found, disabling chroot \
capability checking support for klee-replay.])
fi

AC_LANG_POP([C])

AC_CHECK_HEADERS([selinux/selinux.h],
        AC_SUBST(HAVE_SELINUX, 1),
        AC_SUBST(HAVE_SELINUX, 0))

dnl **************************************************************************
dnl Test for features
dnl **************************************************************************

AC_CHECK_HEADERS([malloc/malloc.h])
AC_CHECK_FUNCS([malloc_zone_statistics])
AC_SEARCH_LIBS(mallinfo,malloc,
               AC_DEFINE([HAVE_MALLINFO],[1],[Define if mallinfo() is available on this platform.]))

dnl **************************************************************************
dnl Find an install of STP
dnl **************************************************************************

AC_ARG_WITH(stp,
  AS_HELP_STRING([--with-stp],
    [Location of STP installation directory]),,
    [AC_MSG_ERROR([The --with-stp=<path> argument is mandatory where <path> is the path \
to the root of your STP install])])

#Check for empty argument
if test "X$with_stp" = X ; then
	AC_MSG_ERROR([<path> cannot be empty in --with-stp=<path>])
else
  stp_root=`(cd $with_stp && pwd) 2> /dev/null`

  #Check for bad path
  if test "X$stp_root" = X ; then
  	AC_MSG_ERROR([Cannot access path $with_stp passed to --with-stp])
  fi

  old_CPPFLAGS="$CPPFLAGS"
  CPPFLAGS="$CPPFLAGS -I$stp_root/include"
  AC_CHECK_HEADER(stp/c_interface.h,, [
         AC_MSG_ERROR([Unable to use stp/c_interface.h header])
  ])
  CPPFLAGS="$old_CPPFLAGS"

  STP_NEEDS_BOOST=0

  # Try old STP
  AC_CHECK_LIB(stp, vc_setInterfaceFlags,, [
         STP_NEEDS_BOOST=1 ; AC_MSG_RESULT([Could not link with libstp. Checking if newer STP is being used])
  ], -L$stp_root/lib)

  dnl Flags for upstream STP which has boost dependency
  UPSTREAM_STP_LINK_FLAGS="-lboost_system -lboost_program_options"
  if test "X$STP_NEEDS_BOOST" != X0 ; then
    # Need to clear cached result
    unset ac_cv_lib_stp_vc_setInterfaceFlags

    AC_CHECK_LIB(stp,
                 vc_setInterfaceFlags,, [
                 AC_MSG_ERROR([Unable to link with libstp. Check config.log to see what went wrong])
    ], -L$stp_root/lib $UPSTREAM_STP_LINK_FLAGS )

    AC_SUBST(UPSTREAM_STP_LINK_FLAGS, $UPSTREAM_STP_LINK_FLAGS)
    AC_SUBST(STP_NEEDS_BOOST, $STP_NEEDS_BOOST)
  else
    AC_MSG_RESULT([Using old STP])
  fi

  AC_SUBST(STP_ROOT,$stp_root)
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)
  AC_SUBST(REQUIRES_RTTI,[[1]])
fi


dnl **************************************************************************
dnl * Create the output files
dnl **************************************************************************

dnl Do special configuration of Makefiles
AC_CONFIG_MAKEFILE(Makefile)
AC_CONFIG_MAKEFILE(Makefile.common)
AC_CONFIG_MAKEFILE(lib/Makefile)
AC_CONFIG_MAKEFILE(runtime/Makefile)
AC_CONFIG_MAKEFILE(test/Makefile)
AC_CONFIG_MAKEFILE(test/Makefile.tests)
AC_CONFIG_MAKEFILE(tools/Makefile)
AC_CONFIG_MAKEFILE(unittests/Makefile)

dnl This must be last
AC_OUTPUT