Download raw body.
UPDATE: cbmc-6.7.1
On Fri Jul 11, 2025 at 09:29:19PM +0200, Rafael Sadowski wrote:
> Update cbmc-6.7.1. Tested on amd64. The motivation was to fix the
> build with upcoming libc++19. Looks like upstream fixed it by:
> https://github.com/diffblue/cbmc/pull/5277
>
> So I decided to update the port instead backporting the fixes.
>
> OK?
>
> Cheers Rafael
>
New diff after feedback. Added missing bin/cbmc and do-test.
2 of 1153 tests failed, 64 tests skipped
Failed test: SIMD1/test.desc
CBMC version 6.7.1 (n/a) 64-bit x86_64 openbsd
Type-checking main
file /usr/lib/clang/19/include/avx512fintrin.h line 404 function _mm512_castpd256_pd512: __builtin_shufflevector expects two vectors as argument
CONVERSION ERROR
Anything we should be aware of?
Rafael
diff --git a/devel/cbmc/Makefile b/devel/cbmc/Makefile
index 5ec7b75de61..527d72c8d59 100644
--- a/devel/cbmc/Makefile
+++ b/devel/cbmc/Makefile
@@ -2,13 +2,12 @@ COMMENT = Bounded Model Checker for C and C++ programs
GH_ACCOUNT = diffblue
GH_PROJECT = cbmc
-GH_TAGNAME = cbmc-5.5
+GH_TAGNAME = cbmc-6.7.1
PKGNAME = ${GH_TAGNAME}
-REVISION = 5
CATEGORIES = devel
-HOMEPAGE = http://www.cprover.org/cbmc/
+HOMEPAGE = https://www.cprover.org/cbmc/
MAINTAINER = Mages Simon <mages.simon@googlemail.com>
@@ -21,7 +20,7 @@ DISTFILES = ${GH_DISTFILE}
DISTFILES.ex = minisat2_2.2.1.orig.tar.gz
SITES.ex = ${SITE_DEBIAN:=main/m/minisat2/}
-# C++11
+# C++17
COMPILER = base-clang ports-gcc
BUILD_DEPENDS = devel/bison
@@ -36,21 +35,26 @@ MAKE_FLAGS = CC="${CC}" \
WRKSRC = ${WRKDIST}/src
+BIN_LIST = cbmc crangler goto-analyzer goto-cc goto-diff goto-harness \
+ goto-inspect goto-instrument goto-synthesizer
+
post-extract:
mv ${WRKDIR}/minisat2-2.2.1 ${WRKDIST}/minisat-2.2.1
cd ${WRKDIST}/minisat-2.2.1; \
patch -z .bak -p1 < ../scripts/minisat-2.2.1-patch
do-install:
-.for i in goto-analyzer goto-cc goto-diff goto-instrument cbmc
+.for i in ${BIN_LIST}
${INSTALL_PROGRAM} ${WRKBUILD}/${i}/${i} ${PREFIX}/bin/
+ ${INSTALL_MAN} ${WRKDIST}/doc/man/${i}.1 ${PREFIX}/man/man1/
.endfor
- ${INSTALL_MAN} ${WRKDIST}/doc/man/cbmc.1 ${PREFIX}/man/man1/
cd ${WRKDIST}/doc/ && find . -type d -exec ${INSTALL_DATA_DIR} \
${PREFIX}/share/doc/cbmc/{} \;
cd ${WRKDIST}/doc/ && find . -type f -exec ${INSTALL_DATA} \
${WRKDIST}/doc/{} ${PREFIX}/share/doc/cbmc/{} \;
- rm ${PREFIX}/share/doc/cbmc/man/cbmc.1
- rmdir ${PREFIX}/share/doc/cbmc/man/
+ rm -rf ${PREFIX}/share/doc/cbmc/man/
+
+do-test:
+ cd ${WRKDIST}/regression/ && ${GMAKE} ${TEST_TARGET}
.include <bsd.port.mk>
diff --git a/devel/cbmc/distinfo b/devel/cbmc/distinfo
index 0d69ca906cd..f3bd5bf9eac 100644
--- a/devel/cbmc/distinfo
+++ b/devel/cbmc/distinfo
@@ -1,4 +1,4 @@
-SHA256 (cbmc-cbmc-5.5.tar.gz) = WpCpr4tTU4rAmDE32eN24uPDjYFYGieJAG8iNYsOnF4=
+SHA256 (cbmc-cbmc-6.7.1.tar.gz) = SGnCfCIbY0eLSpfV11vjHjw1R5emcPQioEBhNZe8mCA=
SHA256 (minisat2_2.2.1.orig.tar.gz) = 5Ur6PBksF1O8gHXAx+Em1cSV2QZuP5CiWICRFJrJykA=
-SIZE (cbmc-cbmc-5.5.tar.gz) = 5274872
+SIZE (cbmc-cbmc-6.7.1.tar.gz) = 9155507
SIZE (minisat2_2.2.1.orig.tar.gz) = 44229
diff --git a/devel/cbmc/patches/patch-src_ansi-c_Makefile b/devel/cbmc/patches/patch-src_ansi-c_Makefile
deleted file mode 100644
index 8c621cbdb32..00000000000
--- a/devel/cbmc/patches/patch-src_ansi-c_Makefile
+++ /dev/null
@@ -1,20 +0,0 @@
-Newer bison includes the defines file in the parser so the name must match.
-
-Index: src/ansi-c/Makefile
---- src/ansi-c/Makefile.orig
-+++ src/ansi-c/Makefile
-@@ -36,12 +36,8 @@ all: ansi-c$(LIBEXT)
-
- ###############################################################################
-
--ansi_c_y.tab.cpp: parser.y
-- $(YACC) $(YFLAGS) $$flags -pyyansi_c -d parser.y -o $@
--
--ansi_c_y.tab.h: ansi_c_y.tab.cpp
-- if [ -e ansi_c_y.tab.hpp ] ; then mv ansi_c_y.tab.hpp ansi_c_y.tab.h ; else \
-- mv ansi_c_y.tab.cpp.h ansi_c_y.tab.h ; fi
-+ansi_c_y.tab.cpp ansi_c_y.tab.h: parser.y
-+ $(YACC) $(YFLAGS) $$flags -pyyansi_c --defines=ansi_c_y.tab.h parser.y -o $@
-
- ansi_c_lex.yy.cpp: scanner.l
- $(LEX) -Pyyansi_c -o$@ scanner.l
diff --git a/devel/cbmc/patches/patch-src_big-int_allocainc_h b/devel/cbmc/patches/patch-src_big-int_allocainc_h
deleted file mode 100644
index 091bab8f433..00000000000
--- a/devel/cbmc/patches/patch-src_big-int_allocainc_h
+++ /dev/null
@@ -1,11 +0,0 @@
---- src/big-int/allocainc.h.orig Sun Oct 16 18:58:41 2016
-+++ src/big-int/allocainc.h Sun Oct 16 18:58:58 2016
-@@ -41,7 +41,7 @@ extern "C" void *alloca (unsigned);
-
- # define alloca(X) __builtin_alloca(X)
-
--#elif defined __FreeBSD__ || defined __FreeBSD_kernel__
-+#elif defined __FreeBSD__ || defined __FreeBSD_kernel__ || defined __OpenBSD__
-
- # include <stdlib.h>
-
diff --git a/devel/cbmc/patches/patch-src_common b/devel/cbmc/patches/patch-src_common
index 3cf12bf75b4..80ab01e44eb 100644
--- a/devel/cbmc/patches/patch-src_common
+++ b/devel/cbmc/patches/patch-src_common
@@ -1,32 +1,12 @@
---- src/common.orig Sat Aug 20 14:08:13 2016
-+++ src/common Fri Oct 14 16:29:34 2016
-@@ -9,6 +9,8 @@ else ifeq ($(uname),Darwin)
- BUILD_ENV_ := OSX
- else ifeq ($(uname),FreeBSD)
- BUILD_ENV_ := FreeBSD
-+else ifeq ($(uname),OpenBSD)
-+ BUILD_ENV_ := OpenBSD
- else ifeq ($(filter-out MINGW32_%, $(uname)),)
- BUILD_ENV_ := MinGW
- else ifeq ($(filter-out CYGWIN_%, $(uname)),)
-@@ -20,7 +22,7 @@ else
- BUILD_ENV_ := $(BUILD_ENV)
- endif
-
--ifeq ($(filter-out Unix MinGW OSX OSX_Universal FreeBSD,$(BUILD_ENV_)),)
-+ifeq ($(filter-out Unix MinGW OSX OSX_Universal FreeBSD OpenBSD,$(BUILD_ENV_)),)
- # Linux-ish
- LIBEXT = .a
- OBJEXT = .o
-@@ -59,6 +61,11 @@ ifeq ($(filter-out OSX OSX_Universal,$(BUILD_ENV_)),)
- else ifeq ($(filter-out FreeBSD,$(BUILD_ENV_)),)
+Index: src/common
+--- src/common.orig
++++ src/common
+@@ -68,7 +68,7 @@ ifeq ($(filter-out OSX OSX_Universal,$(BUILD_ENV_)),)
+ YFLAGS ?= -v
+ else ifeq ($(filter-out FreeBSD OpenBSD,$(BUILD_ENV_)),)
CP_CXXFLAGS +=
- LINKLIB = ar rcT $@ $^
-+ LINKBIN = $(CXX) $(LINKFLAGS) -o $@ -Wl,--start-group $^ -Wl,--end-group $(LIBS)
-+ LINKNATIVE = $(HOSTCXX) -o $@ $^
-+else ifeq ($(filter-out OpenBSD,$(BUILD_ENV_)),)
-+ CP_CXXFLAGS +=
-+ LINKLIB = ar rc $@ $^
+- LINKLIB = llvm-ar rcT $@ $^
++ LINKLIB = ar rcT $@ $^
LINKBIN = $(CXX) $(LINKFLAGS) -o $@ -Wl,--start-group $^ -Wl,--end-group $(LIBS)
- LINKNATIVE = $(HOSTCXX) -o $@ $^
+ LINKNATIVE = $(HOSTCXX) $(HOSTLINKFLAGS) -o $@ $^
ifeq ($(origin CC),default)
diff --git a/devel/cbmc/patches/patch-src_jsil_Makefile b/devel/cbmc/patches/patch-src_jsil_Makefile
deleted file mode 100644
index e7755c34803..00000000000
--- a/devel/cbmc/patches/patch-src_jsil_Makefile
+++ /dev/null
@@ -1,20 +0,0 @@
-Newer bison includes the defines file in the parser so the name must match.
-
-Index: src/jsil/Makefile
---- src/jsil/Makefile.orig
-+++ src/jsil/Makefile
-@@ -19,12 +19,8 @@ all: jsil$(LIBEXT)
- jsil$(LIBEXT): $(OBJ)
- $(LINKLIB)
-
--jsil_y.tab.cpp: parser.y
-- $(YACC) $(YFLAGS) $$flags -pyyjsil -d parser.y -o $@
--
--jsil_y.tab.h: jsil_y.tab.cpp
-- if [ -e jsil_y.tab.hpp ] ; then mv jsil_y.tab.hpp jsil_y.tab.h ; else \
-- mv jsil_y.tab.cpp.h jsil_y.tab.h ; fi
-+jsil_y.tab.cpp jsil_y.tab.h: parser.y
-+ $(YACC) $(YFLAGS) $$flags -pyyjsil --defines=jsil_y.tab.h parser.y -o $@
-
- jsil_lex.yy.cpp: scanner.l
- $(LEX) -Pyyjsil -o$@ scanner.l
diff --git a/devel/cbmc/patches/patch-src_json_Makefile b/devel/cbmc/patches/patch-src_json_Makefile
deleted file mode 100644
index 0053afe9b0d..00000000000
--- a/devel/cbmc/patches/patch-src_json_Makefile
+++ /dev/null
@@ -1,20 +0,0 @@
-Newer bison includes the defines file in the parser so the name must match.
-
-Index: src/json/Makefile
---- src/json/Makefile.orig
-+++ src/json/Makefile
-@@ -15,12 +15,8 @@ all: json$(LIBEXT)
- json$(LIBEXT): $(OBJ)
- $(LINKLIB)
-
--json_y.tab.cpp: parser.y
-- $(YACC) $(YFLAGS) $$flags -pyyjson -d parser.y -o $@
--
--json_y.tab.h: json_y.tab.cpp
-- if [ -e json_y.tab.hpp ] ; then mv json_y.tab.hpp $@ ; else \
-- mv json_y.tab.cpp.h $@ ; fi
-+json_y.tab.cpp json_y.tab.h: parser.y
-+ $(YACC) $(YFLAGS) $$flags -pyyjson --defines=json_y.tab.h parser.y -o $@
-
- json_lex.yy.cpp: scanner.l
- $(LEX) -Pyyjson -o$@ scanner.l
diff --git a/devel/cbmc/patches/patch-src_memory-models_Makefile b/devel/cbmc/patches/patch-src_memory-models_Makefile
deleted file mode 100644
index 03e7602ebea..00000000000
--- a/devel/cbmc/patches/patch-src_memory-models_Makefile
+++ /dev/null
@@ -1,20 +0,0 @@
-Newer bison includes the defines file in the parser so the name must match.
-
-Index: src/memory-models/Makefile
---- src/memory-models/Makefile.orig
-+++ src/memory-models/Makefile
-@@ -16,12 +16,8 @@ all: mmcc$(EXEEXT)
-
- ###############################################################################
-
--mm_y.tab.cpp: parser.y
-- $(YACC) $(YFLAGS) $$flags -pyymm -d parser.y -o $@
--
--mm_y.tab.h: mm_y.tab.cpp
-- if [ -e mm_y.tab.hpp ] ; then mv mm_y.tab.hpp mm_y.tab.h ; else \
-- mv mm_y.tab.cpp.h mm_y.tab.h ; fi
-+mm_y.tab.cpp mm_y.tab.h: parser.y
-+ $(YACC) $(YFLAGS) $$flags -pyymm --defines=mm_y.tab.h parser.y -o $@
-
- mm_lex.yy.cpp: scanner.l
- $(LEX) -Pyymm -o$@ scanner.l
diff --git a/devel/cbmc/patches/patch-src_xmllang_Makefile b/devel/cbmc/patches/patch-src_xmllang_Makefile
deleted file mode 100644
index 39571ddeed3..00000000000
--- a/devel/cbmc/patches/patch-src_xmllang_Makefile
+++ /dev/null
@@ -1,20 +0,0 @@
-Newer bison includes the defines file in the parser so the name must match.
-
-Index: src/xmllang/Makefile
---- src/xmllang/Makefile.orig
-+++ src/xmllang/Makefile
-@@ -15,12 +15,8 @@ all: xmllang$(LIBEXT)
- xmllang$(LIBEXT): $(OBJ)
- $(LINKLIB)
-
--xml_y.tab.cpp: parser.y
-- $(YACC) $(YFLAGS) $$flags -pyyxml -d parser.y -o $@
--
--xml_y.tab.h: xml_y.tab.cpp
-- if [ -e xml_y.tab.hpp ] ; then mv xml_y.tab.hpp $@ ; else \
-- mv xml_y.tab.cpp.h $@ ; fi
-+xml_y.tab.cpp xml_y.tab.h: parser.y
-+ $(YACC) $(YFLAGS) $$flags -pyyxml --defines=xml_y.tab.h parser.y -o $@
-
- xml_lex.yy.cpp: scanner.l
- $(LEX) -Pyyxml -o$@ scanner.l
diff --git a/devel/cbmc/pkg/PLIST b/devel/cbmc/pkg/PLIST
index 9510b0ee0c5..6ff8b3e94c8 100644
--- a/devel/cbmc/pkg/PLIST
+++ b/devel/cbmc/pkg/PLIST
@@ -1,153 +1,133 @@
@bin bin/cbmc
+@bin bin/crangler
@bin bin/goto-analyzer
@bin bin/goto-cc
@bin bin/goto-diff
+@bin bin/goto-harness
+@bin bin/goto-inspect
@bin bin/goto-instrument
+@bin bin/goto-synthesizer
@man man/man1/cbmc.1
+@man man/man1/crangler.1
+@man man/man1/goto-analyzer.1
+@man man/man1/goto-cc.1
+@man man/man1/goto-diff.1
+@man man/man1/goto-harness.1
+@man man/man1/goto-inspect.1
+@man man/man1/goto-instrument.1
+@man man/man1/goto-synthesizer.1
share/doc/cbmc/
-share/doc/cbmc/guide/
-share/doc/cbmc/guide/CBMC-guide.tex
-share/doc/cbmc/html-manual/
-share/doc/cbmc/html-manual/api.shtml
-share/doc/cbmc/html-manual/architecture.shtml
-share/doc/cbmc/html-manual/binsearch.c
-share/doc/cbmc/html-manual/boop-example/
-share/doc/cbmc/html-manual/boop-example/driver.c
-share/doc/cbmc/html-manual/boop-example/driver.h
-share/doc/cbmc/html-manual/boop-example/kdev_t.h
-share/doc/cbmc/html-manual/boop-example/modules.h
-share/doc/cbmc/html-manual/boop-example/spec.c
-share/doc/cbmc/html-manual/c_to_ir.svg
-share/doc/cbmc/html-manual/cbmc-loops.shtml
-share/doc/cbmc/html-manual/cbmc.shtml
-share/doc/cbmc/html-manual/cegar-1.png
-share/doc/cbmc/html-manual/counter.c
-share/doc/cbmc/html-manual/counter.v
-share/doc/cbmc/html-manual/cprover-source.shtml
-share/doc/cbmc/html-manual/expr.c
-share/doc/cbmc/html-manual/expr.svg
-share/doc/cbmc/html-manual/file1.c
-share/doc/cbmc/html-manual/file2.c
-share/doc/cbmc/html-manual/footer.inc
-share/doc/cbmc/html-manual/gcc-wrap.c
-share/doc/cbmc/html-manual/goto-cc-apache.shtml
-share/doc/cbmc/html-manual/goto-cc-linux.shtml
-share/doc/cbmc/html-manual/goto-cc-rockbox.shtml
-share/doc/cbmc/html-manual/goto-cc-variants.shtml
-share/doc/cbmc/html-manual/goto-cc-visual-studio.shtml
-share/doc/cbmc/html-manual/goto-cc.shtml
-share/doc/cbmc/html-manual/goto_program.svg
-share/doc/cbmc/html-manual/header.inc
-share/doc/cbmc/html-manual/highlight/
-share/doc/cbmc/html-manual/highlight/CHANGES.md
-share/doc/cbmc/html-manual/highlight/LICENSE
-share/doc/cbmc/html-manual/highlight/README.md
-share/doc/cbmc/html-manual/highlight/README.ru.md
-share/doc/cbmc/html-manual/highlight/highlight.pack.js
-share/doc/cbmc/html-manual/highlight/styles/
-share/doc/cbmc/html-manual/highlight/styles/agate.css
-share/doc/cbmc/html-manual/highlight/styles/androidstudio.css
-share/doc/cbmc/html-manual/highlight/styles/arduino-light.css
-share/doc/cbmc/html-manual/highlight/styles/arta.css
-share/doc/cbmc/html-manual/highlight/styles/ascetic.css
-share/doc/cbmc/html-manual/highlight/styles/atelier-cave-dark.css
-share/doc/cbmc/html-manual/highlight/styles/atelier-cave-light.css
-share/doc/cbmc/html-manual/highlight/styles/atelier-dune-dark.css
-share/doc/cbmc/html-manual/highlight/styles/atelier-dune-light.css
-share/doc/cbmc/html-manual/highlight/styles/atelier-estuary-dark.css
-share/doc/cbmc/html-manual/highlight/styles/atelier-estuary-light.css
-share/doc/cbmc/html-manual/highlight/styles/atelier-forest-dark.css
-share/doc/cbmc/html-manual/highlight/styles/atelier-forest-light.css
-share/doc/cbmc/html-manual/highlight/styles/atelier-heath-dark.css
-share/doc/cbmc/html-manual/highlight/styles/atelier-heath-light.css
-share/doc/cbmc/html-manual/highlight/styles/atelier-lakeside-dark.css
-share/doc/cbmc/html-manual/highlight/styles/atelier-lakeside-light.css
-share/doc/cbmc/html-manual/highlight/styles/atelier-plateau-dark.css
-share/doc/cbmc/html-manual/highlight/styles/atelier-plateau-light.css
-share/doc/cbmc/html-manual/highlight/styles/atelier-savanna-dark.css
-share/doc/cbmc/html-manual/highlight/styles/atelier-savanna-light.css
-share/doc/cbmc/html-manual/highlight/styles/atelier-seaside-dark.css
-share/doc/cbmc/html-manual/highlight/styles/atelier-seaside-light.css
-share/doc/cbmc/html-manual/highlight/styles/atelier-sulphurpool-dark.css
-share/doc/cbmc/html-manual/highlight/styles/atelier-sulphurpool-light.css
-share/doc/cbmc/html-manual/highlight/styles/brown-paper.css
-share/doc/cbmc/html-manual/highlight/styles/brown-papersq.png
-share/doc/cbmc/html-manual/highlight/styles/codepen-embed.css
-share/doc/cbmc/html-manual/highlight/styles/color-brewer.css
-share/doc/cbmc/html-manual/highlight/styles/dark.css
-share/doc/cbmc/html-manual/highlight/styles/darkula.css
-share/doc/cbmc/html-manual/highlight/styles/default.css
-share/doc/cbmc/html-manual/highlight/styles/docco.css
-share/doc/cbmc/html-manual/highlight/styles/dracula.css
-share/doc/cbmc/html-manual/highlight/styles/far.css
-share/doc/cbmc/html-manual/highlight/styles/foundation.css
-share/doc/cbmc/html-manual/highlight/styles/github-gist.css
-share/doc/cbmc/html-manual/highlight/styles/github.css
-share/doc/cbmc/html-manual/highlight/styles/googlecode.css
-share/doc/cbmc/html-manual/highlight/styles/grayscale.css
-share/doc/cbmc/html-manual/highlight/styles/gruvbox-dark.css
-share/doc/cbmc/html-manual/highlight/styles/gruvbox-light.css
-share/doc/cbmc/html-manual/highlight/styles/hopscotch.css
-share/doc/cbmc/html-manual/highlight/styles/hybrid.css
-share/doc/cbmc/html-manual/highlight/styles/idea.css
-share/doc/cbmc/html-manual/highlight/styles/ir-black.css
-share/doc/cbmc/html-manual/highlight/styles/kimbie.dark.css
-share/doc/cbmc/html-manual/highlight/styles/kimbie.light.css
-share/doc/cbmc/html-manual/highlight/styles/magula.css
-share/doc/cbmc/html-manual/highlight/styles/mono-blue.css
-share/doc/cbmc/html-manual/highlight/styles/monokai-sublime.css
-share/doc/cbmc/html-manual/highlight/styles/monokai.css
-share/doc/cbmc/html-manual/highlight/styles/obsidian.css
-share/doc/cbmc/html-manual/highlight/styles/paraiso-dark.css
-share/doc/cbmc/html-manual/highlight/styles/paraiso-light.css
-share/doc/cbmc/html-manual/highlight/styles/pojoaque.css
-share/doc/cbmc/html-manual/highlight/styles/pojoaque.jpg
-share/doc/cbmc/html-manual/highlight/styles/purebasic.css
-share/doc/cbmc/html-manual/highlight/styles/qtcreator_dark.css
-share/doc/cbmc/html-manual/highlight/styles/qtcreator_light.css
-share/doc/cbmc/html-manual/highlight/styles/railscasts.css
-share/doc/cbmc/html-manual/highlight/styles/rainbow.css
-share/doc/cbmc/html-manual/highlight/styles/school-book.css
-share/doc/cbmc/html-manual/highlight/styles/school-book.png
-share/doc/cbmc/html-manual/highlight/styles/solarized-dark.css
-share/doc/cbmc/html-manual/highlight/styles/solarized-light.css
-share/doc/cbmc/html-manual/highlight/styles/sunburst.css
-share/doc/cbmc/html-manual/highlight/styles/tomorrow-night-blue.css
-share/doc/cbmc/html-manual/highlight/styles/tomorrow-night-bright.css
-share/doc/cbmc/html-manual/highlight/styles/tomorrow-night-eighties.css
-share/doc/cbmc/html-manual/highlight/styles/tomorrow-night.css
-share/doc/cbmc/html-manual/highlight/styles/tomorrow.css
-share/doc/cbmc/html-manual/highlight/styles/vs.css
-share/doc/cbmc/html-manual/highlight/styles/xcode.css
-share/doc/cbmc/html-manual/highlight/styles/xt256.css
-share/doc/cbmc/html-manual/highlight/styles/zenburn.css
-share/doc/cbmc/html-manual/hwsw-inputs.shtml
-share/doc/cbmc/html-manual/hwsw-mapping.shtml
-share/doc/cbmc/html-manual/hwsw-tutorial.shtml
-share/doc/cbmc/html-manual/hwsw.shtml
-share/doc/cbmc/html-manual/index.shtml
-share/doc/cbmc/html-manual/installation-cbmc.shtml
-share/doc/cbmc/html-manual/installation-plugin.shtml
-share/doc/cbmc/html-manual/installation-satabs.shtml
-share/doc/cbmc/html-manual/introduction.shtml
-share/doc/cbmc/html-manual/ireptree.svg
-share/doc/cbmc/html-manual/libraries.shtml
-share/doc/cbmc/html-manual/lock-example-fixed.c
-share/doc/cbmc/html-manual/lock-example.c
-share/doc/cbmc/html-manual/modeling-assertions.shtml
-share/doc/cbmc/html-manual/modeling-floating-point.shtml
-share/doc/cbmc/html-manual/modeling-nondet.shtml
-share/doc/cbmc/html-manual/modeling-pointers.shtml
-share/doc/cbmc/html-manual/properties.shtml
-share/doc/cbmc/html-manual/refinement.png
-share/doc/cbmc/html-manual/ring_buffer1.c
-share/doc/cbmc/html-manual/ring_buffer2.c
-share/doc/cbmc/html-manual/satabs-aeon.shtml
-share/doc/cbmc/html-manual/satabs-background.shtml
-share/doc/cbmc/html-manual/satabs-driver.shtml
-share/doc/cbmc/html-manual/satabs-tutorials.shtml
-share/doc/cbmc/html-manual/satabs.shtml
-share/doc/cbmc/html-manual/states.png
+share/doc/cbmc/ADR/
+share/doc/cbmc/ADR/README.md
+share/doc/cbmc/ADR/cpp_api_modularisation.md
+share/doc/cbmc/ADR/homebrew_tap.md
+share/doc/cbmc/ADR/release_process.md
+share/doc/cbmc/ADR/symex_ready_goto.md
+share/doc/cbmc/API/
+share/doc/cbmc/API/README.md
+share/doc/cbmc/API/util/
+share/doc/cbmc/API/util/piped_process.md
+share/doc/cbmc/C/
+share/doc/cbmc/C/c11-undefined-behavior.html
+share/doc/cbmc/C/n1570-j-2.txt
+share/doc/cbmc/CPPLINT.cfg
+share/doc/cbmc/architectural/
+share/doc/cbmc/architectural/background-concepts.md
+share/doc/cbmc/architectural/cbmc-architecture.md
+share/doc/cbmc/architectural/central-data-structures.md
+share/doc/cbmc/architectural/code-walkthrough.md
+share/doc/cbmc/architectural/compilation-and-development.md
+share/doc/cbmc/architectural/folder-walkthrough.md
+share/doc/cbmc/architectural/front-page.md
+share/doc/cbmc/architectural/goto-program-transformations.md
+share/doc/cbmc/architectural/howto.md
+share/doc/cbmc/architectural/memory-bounds-checking.md
+share/doc/cbmc/architectural/other-tools.md
+share/doc/cbmc/architectural/symex-instructions.md
+share/doc/cbmc/assets/
+share/doc/cbmc/assets/GetLink.png
+share/doc/cbmc/assets/README.md
+share/doc/cbmc/assets/binsearch.c
+share/doc/cbmc/assets/c_to_ir.svg
+share/doc/cbmc/assets/cbmc_style.css
+share/doc/cbmc/assets/cegar-1.png
+share/doc/cbmc/assets/counter.c
+share/doc/cbmc/assets/driver.c
+share/doc/cbmc/assets/driver.h
+share/doc/cbmc/assets/expr.c
+share/doc/cbmc/assets/expr.dot
+share/doc/cbmc/assets/expr.svg
+share/doc/cbmc/assets/file1.c
+share/doc/cbmc/assets/file2.c
+share/doc/cbmc/assets/gcc-wrap.c
+share/doc/cbmc/assets/goto_program.svg
+share/doc/cbmc/assets/ireptree.svg
+share/doc/cbmc/assets/kdev_t.h
+share/doc/cbmc/assets/lock-example-fixed.c
+share/doc/cbmc/assets/lock-example.c
+share/doc/cbmc/assets/modules.h
+share/doc/cbmc/assets/pid.c
+share/doc/cbmc/assets/pid.png
+share/doc/cbmc/assets/refinement.png
+share/doc/cbmc/assets/ring_buffer1.c
+share/doc/cbmc/assets/ring_buffer2.c
+share/doc/cbmc/assets/spec.c
+share/doc/cbmc/assets/states.png
+share/doc/cbmc/assets/xml_spec.md
+share/doc/cbmc/assets/xml_spec.tex
+share/doc/cbmc/assets/xml_spec.xsd
+share/doc/cbmc/cprover-manual/
+share/doc/cbmc/cprover-manual/api.md
+share/doc/cbmc/cprover-manual/binsearch.c
+share/doc/cbmc/cprover-manual/cbmc-assertions.md
+share/doc/cbmc/cprover-manual/cbmc-tutorial.md
+share/doc/cbmc/cprover-manual/cbmc-unwinding.md
+share/doc/cbmc/cprover-manual/file1.c
+share/doc/cbmc/cprover-manual/file2.c
+share/doc/cbmc/cprover-manual/goto-analyzer.md
+share/doc/cbmc/cprover-manual/goto-cc.md
+share/doc/cbmc/cprover-manual/goto-harness.md
+share/doc/cbmc/cprover-manual/index.md
+share/doc/cbmc/cprover-manual/installation.md
+share/doc/cbmc/cprover-manual/introduction.md
+share/doc/cbmc/cprover-manual/jbmc-user-manual.md
+share/doc/cbmc/cprover-manual/lock-example.c
+share/doc/cbmc/cprover-manual/memory-primitives.md
+share/doc/cbmc/cprover-manual/modeling-assumptions.md
+share/doc/cbmc/cprover-manual/modeling-floating-point.md
+share/doc/cbmc/cprover-manual/modeling-mmio.md
+share/doc/cbmc/cprover-manual/modeling-nondeterminism.md
+share/doc/cbmc/cprover-manual/modeling-pointers.md
+share/doc/cbmc/cprover-manual/modeling-shadow-memory.md
+share/doc/cbmc/cprover-manual/properties.md
+share/doc/cbmc/cprover-manual/smt2-incr.md
+share/doc/cbmc/cprover-manual/static-functions.md
+share/doc/cbmc/cprover-manual/test-suite.md
+share/doc/cbmc/cprover-manual/unsound_options.md
+share/doc/cbmc/cprover-manual/visual-studio.md
+share/doc/cbmc/doxygen-root/
+share/doc/cbmc/doxygen-root/.gitignore
+share/doc/cbmc/doxygen-root/DoxygenLayout.xml
+share/doc/cbmc/doxygen-root/Makefile
+share/doc/cbmc/doxygen-root/README.md
+share/doc/cbmc/doxygen-root/contributing.md
+share/doc/cbmc/doxygen-root/developer_guide.md
+share/doc/cbmc/doxygen-root/doxyfile
+share/doc/cbmc/doxygen-root/doxyfile-doc-adr
+share/doc/cbmc/doxygen-root/doxyfile-doc-api
+share/doc/cbmc/doxygen-root/doxyfile-doc-assets
+share/doc/cbmc/doxygen-root/doxyfile-doc-cprover-manual
+share/doc/cbmc/doxygen-root/doxygen-markdown/
+share/doc/cbmc/doxygen-root/doxygen-markdown/append-last-modified-dates.py
+share/doc/cbmc/doxygen-root/doxygen-markdown/doxygen-markdown-preprocessor.py
+share/doc/cbmc/doxygen-root/doxygen-markdown/markdown.sh
+share/doc/cbmc/doxygen-root/doxygen-markdown/pandoc-codeblock-repair.sh
+share/doc/cbmc/doxygen-root/doxygen-markdown/pandoc-cprover-link-filter.py
+share/doc/cbmc/doxygen-root/index.md
+share/doc/cbmc/doxygen-root/installation.md
+share/doc/cbmc/doxygen-root/reference_guide.md
+share/doc/cbmc/doxygen-root/user_guide.md
+share/doc/cbmc/satabs-user-manual.md
share/doc/cbmc/slides/
share/doc/cbmc/slides/cbmc-latex-beamer/
share/doc/cbmc/slides/cbmc-latex-beamer/arrow.pdf
UPDATE: cbmc-6.7.1