Skip to content

Commit c042335

Browse files
committed
Linux build integration test: use 5.17
This includes "libsubcmd: Fix use-after-free for realloc(..., 0)", which was detected by newer GCC versions and that breaks the build.
1 parent 447c0be commit c042335

File tree

1 file changed

+7
-7
lines changed

1 file changed

+7
-7
lines changed

Diff for: integration/linux/compile_linux.sh

+7-7
Original file line numberDiff line numberDiff line change
@@ -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.17, if we do not have it already
24+
[ -d linux_5_17 ] || git clone -b v5.17 --depth=1 https://github.com/torvalds/linux/ linux_5_17
2525

2626
# Prepare compile a part of the kernel with CBMC via one-line-scan
2727
ln -s goto-cc src/goto-cc/goto-ld
@@ -31,7 +31,7 @@ ln -s goto-cc src/goto-cc/goto-g++
3131

3232
configure_linux ()
3333
{
34-
pushd linux_5_10
34+
pushd linux_5_17
3535

3636
cat > kvm-config <<EOF
3737
CONFIG_64BIT=y
@@ -57,10 +57,10 @@ EOF
5757

5858
# Configure kernel, and compile all of it
5959
configure_linux
60-
make -C linux_5_10 bzImage -j $(nproc)
60+
make -C linux_5_17 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_17/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_17 bzImage -j $(nproc) || STATUS=$?
7777
du -h --max-depth=1
7878

7979
# Check for faulty input
8080
ls 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_17/arch/x86/kvm/x86.o | grep "goto-cc" || STATUS=$?
8484

8585
# Propagate failures
8686
exit "$STATUS"

0 commit comments

Comments
 (0)