Fix Makefile-based build for with CUDD

The previous set-up failed to compile (as cudd.h was not found), and
first fixes to make it compile and link resulted in persistent
segmentation faults. These were caused by inconsistent includes as
HAVE_CUDD was only set in selected directories (unlike the CMake
configuration).

Author: tautschnig

jbmc/src/janalyzer/Makefile

@@ -11,6 +11,7 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
       ../$(CPROVER_DIR)/src/pointer-analysis/pointer-analysis$(LIBEXT) \
       ../$(CPROVER_DIR)/src/langapi/langapi$(LIBEXT) \
       ../$(CPROVER_DIR)/src/json/json$(LIBEXT) \
+      ../$(CPROVER_DIR)/src/solvers/solvers$(LIBEXT) \
       ../$(CPROVER_DIR)/src/util/util$(LIBEXT) \
       ..//miniz/miniz$(OBJEXT) \
       ../$(CPROVER_DIR)/src/goto-analyzer/static_show_domain$(OBJEXT) \

jbmc/src/jdiff/Makefile

@@ -28,6 +28,7 @@ OBJ += ../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \
       ../$(CPROVER_DIR)/src/analyses/analyses$(LIBEXT) \
       ../$(CPROVER_DIR)/src/langapi/langapi$(LIBEXT) \
       ../$(CPROVER_DIR)/src/xmllang/xmllang$(LIBEXT) \
+      ../$(CPROVER_DIR)/src/solvers/solvers$(LIBEXT) \
       ../$(CPROVER_DIR)/src/util/util$(LIBEXT) \
       ../miniz/miniz$(OBJEXT) \
       ../$(CPROVER_DIR)/src/json/json$(LIBEXT) \

src/analyses/Makefile

@@ -41,6 +41,10 @@ CLEANFILES = analyses$(LIBEXT)
 
 all: analyses$(LIBEXT)
 
+ifneq ($(CUDD),)
+  OBJ += $(CUDD)/cudd/.libs/libcudd$(LIBEXT) $(CUDD)/cplusplus/.libs/libobj$(LIBEXT)
+endif
+
 ###############################################################################
 
 analyses$(LIBEXT): $(OBJ)

src/common

@@ -195,6 +195,16 @@ ifneq ($(CADICAL),)
 endif
 
 
+ifneq ($(CUDD),)
+  CP_CXXFLAGS += -DHAVE_CUDD
+ifeq ($(CPROVER_DIR),)
+  INCLUDES += -I $(CUDD) -I $(CUDD)/cudd
+else
+  INCLUDES += -I ../$(CPROVER_DIR)/src/solvers/$(CUDD)
+  INCLUDES += -I ../$(CPROVER_DIR)/src/solvers/$(CUDD)/cudd
+endif
+endif
+
 
 first_target: all
 

src/goto-analyzer/Makefile

@@ -19,6 +19,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../langapi/langapi$(LIBEXT) \
       ../json/json$(LIBEXT) \
       ../assembler/assembler$(LIBEXT) \
+      ../solvers/solvers$(LIBEXT) \
       ../util/util$(LIBEXT) \
       # Empty last line
 

src/solvers/Makefile

@@ -44,9 +44,7 @@ ifneq ($(SQUOLEM2),)
 endif
 
 ifneq ($(CUDD),)
-  CUDD_INCLUDE=-I $(CUDD)
   CUDD_LIB=$(CUDD)/cudd/.libs/libcudd$(LIBEXT) $(CUDD)/cplusplus/.libs/libobj$(LIBEXT)
-  CP_CXXFLAGS += -DHAVE_CUDD
 endif
 
 ifneq ($(PICOSAT),)

unit/Makefile

@@ -84,6 +84,7 @@ SRC += analyses/ai/ai.cpp \
 
 INCLUDES= -I ../src/ -I.
 
+CPROVER_DIR = .
 include ../src/config.inc
 include ../src/common