Update lib/cbmc to cbmc#1419

Author: peterschrammel

lib/cbmc

@@ -1,4 +1,4 @@
-DIRS = symex
+DIRS = symex path-symex
 CPROVER_DIR ?= lib/cbmc/src
 export CPROVER_DIR
 

src/Makefile

@@ -8,10 +8,10 @@ SRC = build_goto_trace.cpp \
       var_map.cpp \
       # Empty last line
 
-INCLUDES= -I ..
+INCLUDES= -I ../../$(CPROVER_DIR) -I ../
 
-include ../config.inc
-include ../common
+include ../../$(CPROVER_DIR)/config.inc
+include ../../$(CPROVER_DIR)/common
 
 CLEANFILES = path-symex$(LIBEXT)
 

src/path-symex/Makefile

@@ -20,9 +20,18 @@ OBJ += ../../$(CPROVER_DIR)/ansi-c/ansi-c$(LIBEXT) \
        ../../$(CPROVER_DIR)/goto-symex/rewrite_union$(OBJEXT) \
        ../../$(CPROVER_DIR)/pointer-analysis/dereference$(OBJEXT) \
        ../../$(CPROVER_DIR)/goto-instrument/cover$(OBJEXT) \
-       ../../$(CPROVER_DIR)/path-symex/path-symex$(LIBEXT) \
+       ../../$(CPROVER_DIR)/goto-instrument/cover_basic_blocks$(OBJEXT) \
+       ../../$(CPROVER_DIR)/goto-instrument/cover_filter$(OBJEXT) \
+       ../../$(CPROVER_DIR)/goto-instrument/cover_instrument_branch$(OBJEXT) \
+       ../../$(CPROVER_DIR)/goto-instrument/cover_instrument_condition$(OBJEXT)  \
+       ../../$(CPROVER_DIR)/goto-instrument/cover_instrument_decision$(OBJEXT) \
+       ../../$(CPROVER_DIR)/goto-instrument/cover_instrument_location$(OBJEXT) \
+       ../../$(CPROVER_DIR)/goto-instrument/cover_instrument_mcdc$(OBJEXT) \
+       ../../$(CPROVER_DIR)/goto-instrument/cover_instrument_other$(OBJEXT) \
+       ../../$(CPROVER_DIR)/goto-instrument/cover_util$(OBJEXT) \
        ../../$(CPROVER_DIR)/miniz/miniz$(OBJEXT) \
-       ../../$(CPROVER_DIR)/json/json$(LIBEXT)
+       ../../$(CPROVER_DIR)/json/json$(LIBEXT) \
+       ../path-symex/path-symex$(LIBEXT)
 
 INCLUDES= -I .. -I ../../$(CPROVER_DIR)
 

src/symex/Makefile

@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-programs/goto_model.h>
 #include <goto-programs/show_goto_functions.h>
+#include <goto-programs/rebuild_goto_start_function.h>
 
 #include <analyses/goto_check.h>