Add goto-bmc and libcprover-cpp to Makefile builds

Ensure both build infrastructures remain in sync.

Author: tautschnig

src/Makefile

@@ -7,6 +7,7 @@ DIRS = analyses \
        cprover \
        crangler \
        goto-analyzer \
+       goto-bmc \
        goto-cc \
        goto-checker \
        goto-diff \
@@ -20,6 +21,7 @@ DIRS = analyses \
        json \
        json-symtab-language \
        langapi \
+       libcprover-cpp \
        linking \
        memory-analyzer \
        pointer-analysis \
@@ -34,6 +36,7 @@ all: cbmc.dir \
      cprover.dir \
      crangler.dir \
      goto-analyzer.dir \
+     goto-bmc.dir \
      goto-cc.dir \
      goto-diff.dir \
      goto-instrument.dir \
@@ -114,6 +117,10 @@ goto-synthesizer.dir: languages util.dir goto-programs.dir langapi.dir \
                     json.dir goto-checker.dir \
                     goto-instrument.dir
 
+goto-bmc.dir: libcprover-cpp.dir
+
+libcprover-cpp.dir: cbmc.dir
+
 # building for a particular directory
 
 $(patsubst %, %.dir, $(DIRS)):

src/goto-bmc/Makefile

@@ -0,0 +1,29 @@
+SRC = \
+  goto_bmc_main.cpp \
+  goto_bmc_parse_options.cpp \
+  # Empty last line
+
+OBJ += \
+  ../libcprover-cpp/libcprover-cpp$(LIBEXT) \
+  # Empty last line
+
+INCLUDES= -I .. -I ../libcprover-cpp
+
+LIBS =
+
+CLEANFILES = goto-bmc$(EXEEXT)
+
+include ../config.inc
+include ../common
+
+all: goto-bmc$(EXEEXT)
+
+###############################################################################
+
+goto-bmc$(EXEEXT): $(OBJ)
+	$(LINKBIN)
+
+.PHONY: goto-bmc-mac-signed
+
+goto-bmc-mac-signed: goto-bmc$(EXEEXT)
+	codesign -v -s $(OSX_IDENTITY) goto-bmc$(EXEEXT)

src/libcprover-cpp/Makefile

@@ -0,0 +1,61 @@
+SRC = \
+  api.cpp \
+  api_options.cpp \
+  verification_result.cpp \
+  # Empty last line
+
+OBJ += \
+  ../analyses/analyses$(LIBEXT) \
+  ../ansi-c/ansi-c$(LIBEXT) \
+  ../assembler/assembler$(LIBEXT) \
+  ../big-int/big-int$(LIBEXT) \
+  ../goto-checker/goto-checker$(LIBEXT) \
+  ../goto-instrument/cover$(OBJEXT) \
+  ../goto-instrument/cover_basic_blocks$(OBJEXT) \
+  ../goto-instrument/cover_filter$(OBJEXT) \
+  ../goto-instrument/cover_instrument_assume$(OBJEXT) \
+  ../goto-instrument/cover_instrument_branch$(OBJEXT) \
+  ../goto-instrument/cover_instrument_condition$(OBJEXT) \
+  ../goto-instrument/cover_instrument_decision$(OBJEXT) \
+  ../goto-instrument/cover_instrument_location$(OBJEXT) \
+  ../goto-instrument/cover_instrument_mcdc$(OBJEXT) \
+  ../goto-instrument/cover_instrument_other$(OBJEXT) \
+  ../goto-instrument/cover_util$(OBJEXT) \
+  ../goto-instrument/full_slicer$(OBJEXT) \
+  ../goto-instrument/nondet_static$(OBJEXT) \
+  ../goto-instrument/reachability_slicer$(OBJEXT) \
+  ../goto-instrument/source_lines$(OBJEXT) \
+  ../goto-instrument/unwindset$(OBJEXT) \
+  ../goto-programs/goto-programs$(LIBEXT) \
+  ../goto-symex/goto-symex$(LIBEXT) \
+  ../jsil/jsil$(LIBEXT) \
+  ../json-symtab-language/json-symtab-language$(LIBEXT) \
+  ../json/json$(LIBEXT) \
+  ../langapi/langapi$(LIBEXT) \
+  ../linking/linking$(LIBEXT) \
+  ../pointer-analysis/add_failed_symbols$(OBJEXT) \
+  ../pointer-analysis/goto_program_dereference$(OBJEXT) \
+  ../pointer-analysis/value_set$(OBJEXT) \
+  ../pointer-analysis/value_set_analysis_fi$(OBJEXT) \
+  ../pointer-analysis/value_set_dereference$(OBJEXT) \
+  ../pointer-analysis/value_set_domain_fi$(OBJEXT) \
+  ../pointer-analysis/value_set_fi$(OBJEXT) \
+  ../solvers/solvers$(LIBEXT) \
+  ../statement-list/statement-list$(LIBEXT) \
+  ../util/util$(LIBEXT) \
+  ../xmllang/xmllang$(LIBEXT) \
+  # Empty last line
+
+INCLUDES = -I ..
+
+include ../config.inc
+include ../common
+
+CLEANFILES = libcprover-cpp$(LIBEXT)
+
+all: libcprover-cpp$(LIBEXT)
+
+###############################################################################
+
+libcprover-cpp$(LIBEXT): $(OBJ)
+	$(LINKLIB)