"Application of Software Verification to OpenBSD Network Modules"
Instructions for reproducing the results

Setting up the OpenBSD build environment
1. Download and install OpenBSD 6.3 (using a virtual environment is OK)
Link: https://ftp.hostserver.de/pub/OpenBSD/6.3/amd64/install63.iso
Don't forget to remove the installation media after the install
The next steps are done on the OpenBSD machine
2. Install git with `pkg_add git` as root (man doas or su)
Don't forget to add an install url (man installurl)
e.g. `echo 'https://ftp.hostserver.de/pub/OpenBSD' > /etc/installurl`
3. Download the OpenBSD source i.e. from GitHub
with `git clone 'https://github.com/openbsd/src'`
The path of the 'src' directory is important later on.

Building CPAchecker (on a Linux machine)
1. get the CPAchecker source code
2. check out the following version:
svn r29066
git 0e11ea4a504ca212fa2507a49e5c1aec909ca607
3. apply the required patches `git apply cpachecker.patch`
4. build with `ant`
A module can be tested with
`./scripts/cpa.sh -heap 8G -stack 1G -openbsd--memorysafety module.c`
Don't forget to set the JAVA environment variable.

Creating a module
The following description are shell commands that can be run on OpenBSD,
the preproc.pl program, the code_adjustments.patch file and the stubs
directory and the module folders are provided with this README
# $stubs is the stubs directiory provided with this README
# $module is the module folder to create, e.g.  `module=etherip`
module=`readlink -f $module`
stubs=`readlink -f $stubs`
SRC=`readlink -f XXX` # XXX is the 'src' folder

# create the header files for the current version
cd $SRC/sys/arch/amd64/compile/GENERIC.MP
make obj
make config

# check out a version before the bug was fixed
cd $SRC
git checkout `cat $module/patched_revision`~
# remove the ~ to check out the patched version

# apply additional adjustments to work around errors in CPAchecker
git apply $module/code_adjustments.patch

# don't pollute the src directory.
cd $module 

# create a single C file
cat $stubs/percpu.c $stubs/mbuf.c $stubs/mbuf2.c $stubs/pool.c \
$(eval echo $(cat $module/required_files)) $module/main.c > module.c

# ensure that header files are only included once
perl -ni preproc.pl module.c

# preprocess the file
cc -g -Werror -Wall -Wimplicit-function-declaration \
-Wno-uninitialized -Wno-pointer-sign  -Wno-address-of-packed-member \
-Wno-constant-conversion  -Wframe-larger-than=2047 -mcmodel=kernel \
-mno-red-zone -mno-sse2 -mno-sse -mno-3dnow  -mno-mmx -msoft-float \
-fno-omit-frame-pointer -ffreestanding -fno-pie -O2 -pipe -nostdinc \
-I$SRC/sys -I$SRC/sys/arch -DDIAGNOSTIC -DKTRACE -DACCOUNTING \
-DKMEMSTATS -DPTRACE -DPOOL_DEBUG -DCRYPTO -DSYSVMSG -DSYSVSEM \
-DSYSVSHM -DUVM_SWAP_ENCRYPT -DFFS -DFFS2 -DFFS_SOFTUPDATES \
-DUFS_DIRHASH -DQUOTA -DEXT2FS -DMFS -DNFSCLIENT -DNFSSERVER -DCD9660 \
-DUDF -DMSDOSFS -DFIFO -DFUSE -DSOCKET_SPLICE -DTCP_ECN -DINET6 \
-DPPP_BSDCOMP -DPPP_DEFLATE -DPIPEX -DMROUTING -DBOOT_CONFIG \
-DUSER_PCICONF -DAPERTURE -DMTRR -DNTFS -DHIBERNATE -DPCIVERBOSE \
-DUSBVERBOSE -DWSDISPLAY_COMPAT_USL -DWSDISPLAY_COMPAT_RAWKBD \
-DWSDISPLAY_DEFAULTSCREENS="6" -DX86EMU -DONEWIREVERBOSE \
-DMULTIPROCESSOR -DMAXUSERS=80 -D_KERNEL -MD -MP  -c module.c -I$SRC/ \
sys/arch/amd64/compile/GENERIC.MP/obj -E -P  -o module_preproc.c

# module_preproc.c can now be used with CPAchecker