@@ -20,8 +20,8 @@ make -C src CXX='ccache /usr/bin/g++' cbmc.dir goto-cc.dir goto-diff.dir -j$(npr
2020# Get one-line-scan, if we do not have it already
2121[ -d one-line-scan ] || git clone https://github.com/awslabs/one-line-scan.git one-line-scan
2222
23- # Get Linux v5.10 , if we do not have it already
24- [ -d linux_5_10 ] || git clone -b v5.10 --depth=1 https://github.com/torvalds/linux/ linux_5_10
23+ # Get Linux v5.16.11 , if we do not have it already
24+ [ -d linux_5_16_11 ] || git clone -b v5.16.11 --depth=1 https://github.com/torvalds/linux/ linux_5_16_11
2525
2626# Prepare compile a part of the kernel with CBMC via one-line-scan
2727ln -s goto-cc src/goto-cc/goto-ld
@@ -31,7 +31,7 @@ ln -s goto-cc src/goto-cc/goto-g++
3131
3232configure_linux ()
3333{
34- pushd linux_5_10
34+ pushd linux_5_16_11
3535
3636 cat > kvm-config << EOF
3737CONFIG_64BIT=y
5757
5858# Configure kernel, and compile all of it
5959configure_linux
60- make -C linux_5_10 bzImage -j $( nproc)
60+ make -C linux_5_16_11 bzImage -j $( nproc)
6161
6262# Clean files we want to be able to re-compile
63- find linux_5_10 /arch/x86/kvm/ -name " *.o" -delete
63+ find linux_5_16_11 /arch/x86/kvm/ -name " *.o" -delete
6464
6565# Compile Linux with CBMC via one-line-scan, and check for goto-cc section
6666# Re-Compile with goto-cc, and measure disk space
@@ -73,14 +73,14 @@ one-line-scan/one-line-scan \
7373 --trunc-existing \
7474 --extra-cflags -Wno-error \
7575 -o CPROVER -j 5 -- \
76- make -C linux_5_10 bzImage -j $( nproc) || STATUS=$?
76+ make -C linux_5_16_11 bzImage -j $( nproc) || STATUS=$?
7777du -h --max-depth=1
7878
7979# Check for faulty input
8080ls CPROVER/faultyInput/* || true
8181
8282# Check for produced output in the files we deleted above
83- objdump -h linux_5_10 /arch/x86/kvm/x86.o | grep " goto-cc" || STATUS=$?
83+ objdump -h linux_5_16_11 /arch/x86/kvm/x86.o | grep " goto-cc" || STATUS=$?
8484
8585# Propagate failures
8686exit " $STATUS "
0 commit comments