aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorHoang M. Le <hle@informatik.uni-bremen.de>2016-05-26 14:04:55 +0200
committerHoang M. Le <hle@informatik.uni-bremen.de>2016-06-10 10:24:00 +0200
commitb30c06f9115bfcfea7a5d4d7609a25778adc573e (patch)
tree10d65c6f2642ce25687b106e471956361a3366ee
parent8a43b34c48d5d0507be51e3a7a1eac87fb60e0dc (diff)
downloadklee-b30c06f9115bfcfea7a5d4d7609a25778adc573e.tar.gz
update Makefile for metaSMT
-rw-r--r--Makefile.common8
-rw-r--r--MetaSMT.mk16
-rwxr-xr-xlib/Solver/Makefile10
3 files changed, 8 insertions, 26 deletions
diff --git a/Makefile.common b/Makefile.common
index 9bc850ba..cf7bdcf7 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -78,11 +78,5 @@ ifeq ($(ENABLE_UCLIBC),1)
endif
# For metaSMT
-ifeq ($(ENABLE_METASMT),1)
- include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile
- LD.Flags += -L$(METASMT_ROOT)/lib
- CXX.Flags += -DBOOST_HAS_GCC_TR1 -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS
- CXX.Flags := $(filter-out -fno-exceptions,$(CXX.Flags))
- CXX.Flags += $(metaSMT_INCLUDES)
-endif
+include $(PROJ_SRC_ROOT)/MetaSMT.mk
diff --git a/MetaSMT.mk b/MetaSMT.mk
index 94dd398a..80f28a9b 100644
--- a/MetaSMT.mk
+++ b/MetaSMT.mk
@@ -1,17 +1,11 @@
# This file contains common code for linking against MetaSMT
#
-# FIXME: This is a horribly fragile hack.
-# Instead the detection of what solvers the build of MetaSMT supports should be
-# done by the configure script and then the appropriate compiler flags should
-# be emitted to Makefile.config for consumption here.
+# Consume flags generated by metaSMT here.
ifeq ($(ENABLE_METASMT),1)
include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile
- LD.Flags += -L$(METASMT_ROOT)/../../deps/Z3-4.1/lib \
- -L$(METASMT_ROOT)/../../deps/boolector-1.5.118/lib \
- -L$(METASMT_ROOT)/../../deps/minisat-git/lib/ \
- -L$(METASMT_ROOT)/../../deps/boost-1_52_0/lib \
- -L$(METASMT_ROOT)/../../deps/stp-svn/lib
- CXX.Flags += -DBOOST_HAS_GCC_TR1
+ LD.Flags += $(metaSMT_LDFLAGS)
+ CXX.Flags += $(metaSMT_CXXFLAGS)
+ CXX.Flags += $(metaSMT_INCLUDES)
CXX.Flags := $(filter-out -fno-exceptions,$(CXX.Flags))
- LIBS += -lgomp -lboost_iostreams -lboost_thread -lboost_system -lmetaSMT -lz3 -lstp -lrt -lboolector -lminisat_core
+ LIBS += $(metaSMT_LDLIBS)
endif
diff --git a/lib/Solver/Makefile b/lib/Solver/Makefile
index a44b4f6e..715f4b2d 100755
--- a/lib/Solver/Makefile
+++ b/lib/Solver/Makefile
@@ -16,11 +16,5 @@ NO_INSTALL=1
include $(LEVEL)/Makefile.common
-ifeq ($(ENABLE_METASMT),1)
- include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile
- CXX.Flags += -DBOOST_HAS_GCC_TR1
- CXX.Flags := $(filter-out -fno-exceptions,$(CXX.Flags))
- CXX.Flags := $(filter-out -fno-rtti,$(CXX.Flags))
- CXX.Flags += $(metaSMT_CXXFLAGS)
- CXX.Flags += $(metaSMT_INCLUDES)
-endif
+include $(PROJ_SRC_ROOT)/MetaSMT.mk
+