From: Rafael Sadowski <rafael@sizeofvoid.org>
Subject: UPDATE: cbmc-6.7.1
To: ports@openbsd.org
Cc: Mages Simon <mages.simon@googlemail.com>
Date: Fri, 11 Jul 2025 21:29:19 +0200

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

Index: Makefile
===================================================================
RCS file: /cvs/ports/devel/cbmc/Makefile,v
diff -u -p -u -p -r1.16 Makefile
--- Makefile	21 Sep 2023 09:49:49 -0000	1.16
+++ Makefile	11 Jul 2025 19:26:42 -0000
@@ -2,13 +2,12 @@ COMMENT =	Bounded Model Checker for C an
 
 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,23 @@ MAKE_FLAGS =	CC="${CC}" \
 
 WRKSRC =	${WRKDIST}/src
 
+BIN_LIST =	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/
 
 .include <bsd.port.mk>
Index: distinfo
===================================================================
RCS file: /cvs/ports/devel/cbmc/distinfo,v
diff -u -p -u -p -r1.2 distinfo
--- distinfo	30 Nov 2021 10:10:06 -0000	1.2
+++ distinfo	11 Jul 2025 19:26:42 -0000
@@ -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
Index: patches/patch-src_ansi-c_Makefile
===================================================================
RCS file: patches/patch-src_ansi-c_Makefile
diff -N patches/patch-src_ansi-c_Makefile
--- patches/patch-src_ansi-c_Makefile	11 Mar 2022 18:49:48 -0000	1.3
+++ /dev/null	1 Jan 1970 00:00:00 -0000
@@ -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
Index: patches/patch-src_big-int_allocainc_h
===================================================================
RCS file: patches/patch-src_big-int_allocainc_h
diff -N patches/patch-src_big-int_allocainc_h
--- patches/patch-src_big-int_allocainc_h	11 Mar 2022 18:49:48 -0000	1.2
+++ /dev/null	1 Jan 1970 00:00:00 -0000
@@ -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>
- 
Index: patches/patch-src_common
===================================================================
RCS file: /cvs/ports/devel/cbmc/patches/patch-src_common,v
diff -u -p -u -p -r1.2 patch-src_common
--- patches/patch-src_common	11 Mar 2022 18:49:48 -0000	1.2
+++ patches/patch-src_common	11 Jul 2025 19:26:42 -0000
@@ -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)
Index: patches/patch-src_jsil_Makefile
===================================================================
RCS file: patches/patch-src_jsil_Makefile
diff -N patches/patch-src_jsil_Makefile
--- patches/patch-src_jsil_Makefile	11 Mar 2022 18:49:48 -0000	1.3
+++ /dev/null	1 Jan 1970 00:00:00 -0000
@@ -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
Index: patches/patch-src_json_Makefile
===================================================================
RCS file: patches/patch-src_json_Makefile
diff -N patches/patch-src_json_Makefile
--- patches/patch-src_json_Makefile	11 Mar 2022 18:49:48 -0000	1.3
+++ /dev/null	1 Jan 1970 00:00:00 -0000
@@ -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
Index: patches/patch-src_memory-models_Makefile
===================================================================
RCS file: patches/patch-src_memory-models_Makefile
diff -N patches/patch-src_memory-models_Makefile
--- patches/patch-src_memory-models_Makefile	11 Mar 2022 18:49:48 -0000	1.3
+++ /dev/null	1 Jan 1970 00:00:00 -0000
@@ -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
Index: patches/patch-src_xmllang_Makefile
===================================================================
RCS file: patches/patch-src_xmllang_Makefile
diff -N patches/patch-src_xmllang_Makefile
--- patches/patch-src_xmllang_Makefile	11 Mar 2022 18:49:48 -0000	1.3
+++ /dev/null	1 Jan 1970 00:00:00 -0000
@@ -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
Index: pkg/PLIST
===================================================================
RCS file: /cvs/ports/devel/cbmc/pkg/PLIST,v
diff -u -p -u -p -r1.2 PLIST
--- pkg/PLIST	11 Mar 2022 18:49:48 -0000	1.2
+++ pkg/PLIST	11 Jul 2025 19:26:42 -0000
@@ -1,153 +1,131 @@
-@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
-@man man/man1/cbmc.1
+@bin bin/goto-synthesizer
+@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