CONTRACTS: add doc for loop assigns inference #10600

Workflow file for this run

.github/workflows/pull-request-checks.yaml at dfab451

	name: Build and Test CBMC
	on:
	push:
	branches: [ develop ]
	pull_request:
	branches: [ develop ]
	env:
	cvc5-version: "1.1.2"
	linux-vcpus: 4
	windows-vcpus: 4

	jobs:
	# This job takes approximately 15 to 40 minutes
	check-ubuntu-20_04-make-gcc:
	runs-on: ubuntu-20.04
	steps:
	- uses: actions/checkout@v4
	with:
	submodules: recursive
	- name: Fetch dependencies
	env:
	# This is needed in addition to -yq to prevent apt-get from asking for
	# user input
	DEBIAN_FRONTEND: noninteractive
	run: \|
	sudo apt-get update
	sudo apt-get install --no-install-recommends -yq gcc gdb g++ maven jq flex bison libxml2-utils ccache cmake z3
	- name: Confirm z3 solver is available and log the version installed
	run: z3 --version
	- name: Download cvc-5 from the releases page and make sure it can be deployed
	run: \|
	wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-static.zip
	unzip -j -d /usr/local/bin cvc5-Linux-static.zip cvc5-Linux-static/bin/cvc5
	rm cvc5-Linux-static.zip
	cvc5 --version
	- name: Prepare ccache
	uses: actions/cache@v4
	with:
	save-always: true
	path: .ccache
	key: ${{ runner.os }}-20.04-make-${{ github.ref }}-${{ github.sha }}-PR
	restore-keys: \|
	${{ runner.os }}-20.04-make-${{ github.ref }}
	${{ runner.os }}-20.04-make
	- name: ccache environment
	run: \|
	echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
	echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
	- name: Zero ccache stats and limit in size
	run: ccache -z --max-size=500M
	- name: Build with make
	run: \|
	git clone https://github.com/conp-solutions/riss riss.git
	cmake -Hriss.git -Briss.git/release -DCMAKE_BUILD_TYPE=Release
	make -C riss.git/release riss-coprocessor-lib-static -j${{env.linux-vcpus}}
	make -C src -j${{env.linux-vcpus}} CXX="ccache g++" LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss
	make -C jbmc/src -j${{env.linux-vcpus}} CXX="ccache g++" LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss

	make -C unit -j${{env.linux-vcpus}} CXX="ccache g++" LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss

	make -C jbmc/unit -j${{env.linux-vcpus}} CXX="ccache g++" LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss
	- name: Print ccache stats
	run: ccache -s
	- name: Checking completeness of help output
	run: scripts/check_help.sh g++
	- name: Run unit tests
	run: \|
	make -C unit test IPASIR=$PWD/riss.git/riss
	make -C jbmc/unit test IPASIR=$PWD/riss.git/riss
	echo "Running expected failure tests"
	make TAGS="[!shouldfail]" -C unit test IPASIR=$PWD/riss.git/riss
	make TAGS="[!shouldfail]" -C jbmc/unit test IPASIR=$PWD/riss.git/riss
	- name: Run regression tests
	run: \|
	make -C regression test-parallel JOBS=${{env.linux-vcpus}} LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss
	make -C regression/cbmc test-paths-lifo
	env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2
	make -C jbmc/regression test-parallel JOBS=${{env.linux-vcpus}}
	- name: Check cleanup
	run: \|
	make -C src clean IPASIR=$PWD/riss.git/riss
	make -C jbmc/src clean IPASIR=$PWD/riss.git/riss
	rm -r riss.git
	rm src/goto-cc/goto-ld
	make -C unit clean
	make -C regression clean
	make -C jbmc/unit clean
	make -C jbmc/regression clean
	if [[ $(git status --ignored --porcelain \| grep -v .ccache/) ]] ; then
	git status --ignored
	exit 1
	fi

	# This job takes approximately 25 to 34 minutes
	check-ubuntu-20_04-make-clang:
	runs-on: ubuntu-20.04
	env:
	CC: "ccache /usr/bin/clang"
	CXX: "ccache /usr/bin/clang++"
	steps:
	- uses: actions/checkout@v4
	with:
	submodules: recursive
	- name: Fetch dependencies
	env:
	# This is needed in addition to -yq to prevent apt-get from asking for
	# user input
	DEBIAN_FRONTEND: noninteractive
	run: \|
	sudo apt-get update
	sudo apt-get install --no-install-recommends -yq clang-10 clang++-10 gdb maven jq flex bison libxml2-utils cpanminus ccache z3
	make -C src minisat2-download cadical-download
	cpanm Thread::Pool::Simple
	- name: Confirm z3 solver is available and log the version installed
	run: z3 --version
	- name: Download cvc-5 from the releases page and make sure it can be deployed
	run: \|
	wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-static.zip
	unzip -j -d /usr/local/bin cvc5-Linux-static.zip cvc5-Linux-static/bin/cvc5
	rm cvc5-Linux-static.zip
	cvc5 --version
	- name: Prepare ccache
	uses: actions/cache@v4
	with:
	save-always: true
	path: .ccache
	key: ${{ runner.os }}-20.04-make-clang-${{ github.ref }}-${{ github.sha }}-PR
	restore-keys: \|
	${{ runner.os }}-20.04-make-clang-${{ github.ref }}
	${{ runner.os }}-20.04-make-clang
	- name: ccache environment
	run: \|
	echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
	echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
	- name: Zero ccache stats and limit in size
	run: ccache -z --max-size=500M
	- name: Build with make
	run: \|
	make -C src -j${{env.linux-vcpus}} MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical
	make -C unit -j${{env.linux-vcpus}}
	make -C jbmc/src -j${{env.linux-vcpus}}
	make -C jbmc/unit -j${{env.linux-vcpus}}
	- name: Print ccache stats
	run: ccache -s
	- name: Run unit tests
	run: \|
	make -C unit test
	make -C jbmc/unit test
	make TAGS="[z3]" -C unit test
	- name: Run expected failure unit tests
	run: \|
	make TAGS="[!shouldfail]" -C unit test
	make TAGS="[!shouldfail]" -C jbmc/unit test
	- name: Run regression tests
	run: \|
	make -C regression test-parallel JOBS=${{env.linux-vcpus}}
	make -C regression/cbmc test-paths-lifo
	env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2
	make -C jbmc/regression test-parallel JOBS=${{env.linux-vcpus}}

	# This job has been copied from the one above it, and modified to only build CBMC
	# and run the `regression/cbmc/` regression tests against Z3. The rest of the tests
	# (unit/regression) have been stripped based on the rationale that they are going
	# to be run by the job above, which is basically the same, but more comprehensive.
	# The reason we opted for a new job is that adding a `test-z3` step to the current
	# jobs increases the job runtime to unacceptable levels (over 2hrs).
	# This job takes approximately 3 to 18 minutes
	check-ubuntu-20_04-make-clang-smt-z3:
	runs-on: ubuntu-20.04
	env:
	CC: "ccache /usr/bin/clang"
	CXX: "ccache /usr/bin/clang++"
	steps:
	- uses: actions/checkout@v4
	with:
	submodules: recursive
	- name: Fetch dependencies
	env:
	DEBIAN_FRONTEND: noninteractive
	run: \|
	sudo apt-get update
	sudo apt-get install --no-install-recommends -yq clang-10 clang++-10 gdb maven jq flex bison libxml2-utils cpanminus ccache z3
	make -C src minisat2-download
	cpanm Thread::Pool::Simple
	- name: Confirm z3 solver is available and log the version installed
	run: z3 --version
	- name: Prepare ccache
	uses: actions/cache@v4
	with:
	save-always: true
	path: .ccache
	key: ${{ runner.os }}-20.04-make-clang-${{ github.ref }}-${{ github.sha }}-PR
	restore-keys: \|
	${{ runner.os }}-20.04-make-clang-${{ github.ref }}
	${{ runner.os }}-20.04-make-clang
	- name: ccache environment
	run: \|
	echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
	echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
	- name: Zero ccache stats and limit in size
	run: ccache -z --max-size=500M
	- name: Build with make
	run: make -C src -j${{env.linux-vcpus}}
	- name: Print ccache stats
	run: ccache -s
	- name: Run regression/cbmc tests with z3 as the backend
	run: make -C regression/cbmc test-z3

	# This job takes approximately 17 to 42 minutes
	check-ubuntu-20_04-cmake-gcc:
	runs-on: ubuntu-20.04
	steps:
	- uses: actions/checkout@v4
	with:
	submodules: recursive
	- name: Fetch dependencies
	env:
	# This is needed in addition to -yq to prevent apt-get from asking for
	# user input
	DEBIAN_FRONTEND: noninteractive
	run: \|
	sudo apt-get update
	sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc gdb g++ maven flex bison libxml2-utils dpkg-dev ccache doxygen graphviz z3
	- name: Confirm z3 solver is available and log the version installed
	run: z3 --version
	- name: Download cvc-5 from the releases page and make sure it can be deployed
	run: \|
	wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-static.zip
	unzip -j -d /usr/local/bin cvc5-Linux-static.zip cvc5-Linux-static/bin/cvc5
	rm cvc5-Linux-static.zip
	cvc5 --version
	- name: Prepare ccache
	uses: actions/cache@v4
	with:
	save-always: true
	path: .ccache
	key: ${{ runner.os }}-20.04-Release-${{ github.ref }}-${{ github.sha }}-PR
	restore-keys: \|
	${{ runner.os }}-20.04-Release-${{ github.ref }}
	${{ runner.os }}-20.04-Release
	- name: ccache environment
	run: \|
	echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
	echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
	- name: Configure using CMake
	run: cmake -S . -B build -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -Dsat_impl="minisat2;cadical"
	- name: Check that doc task works
	run: ninja -C build doc
	- name: Zero ccache stats and limit in size
	run: ccache -z --max-size=500M
	- name: Build with Ninja
	run: ninja -C build -j${{env.linux-vcpus}}
	- name: Print ccache stats
	run: ccache -s
	- name: Checking completeness of help output
	run: scripts/check_help.sh /usr/bin/g++ build/bin
	- name: Check if package building works
	run: \|
	cd build
	ninja package
	ls *.deb
	- name: Run tests
	run: cd build; ctest . -V -L CORE -j${{env.linux-vcpus}}
	- name: Check cleanup
	run: \|
	rm -r build
	rm scripts/bash-autocomplete/cbmc.sh
	make -C unit clean
	make -C regression clean
	make -C jbmc/regression clean
	if [[ $(git status --ignored --porcelain \| grep -v .ccache/) ]] ; then
	git status --ignored
	exit 1
	fi

	# This job takes approximately 20 to 38 minutes
	check-ubuntu-22_04-make-clang:
	runs-on: ubuntu-22.04
	env:
	CC: "ccache /usr/bin/clang"
	CXX: "ccache /usr/bin/clang++"
	steps:
	- uses: actions/checkout@v4
	with:
	submodules: recursive
	- name: Fetch dependencies
	env:
	# This is needed in addition to -yq to prevent apt-get from asking for
	# user input
	DEBIAN_FRONTEND: noninteractive
	run: \|
	sudo apt-get update
	sudo apt-get install --no-install-recommends -yq clang clang-14 gdb maven jq flex bison libxml2-utils cpanminus ccache z3
	make -C src minisat2-download cadical-download
	cpanm Thread::Pool::Simple
	- name: Confirm z3 solver is available and log the version installed
	run: z3 --version
	- name: Download cvc-5 from the releases page and make sure it can be deployed
	run: \|
	wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-static.zip
	unzip -j -d /usr/local/bin cvc5-Linux-static.zip cvc5-Linux-static/bin/cvc5
	rm cvc5-Linux-static.zip
	cvc5 --version
	- name: Prepare ccache
	uses: actions/cache@v4
	with:
	save-always: true
	path: .ccache
	key: ${{ runner.os }}-22.04-make-clang-${{ github.ref }}-${{ github.sha }}-PR
	restore-keys: \|
	${{ runner.os }}-22.04-make-clang-${{ github.ref }}
	${{ runner.os }}-22.04-make-clang
	- name: ccache environment
	run: \|
	echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
	echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
	- name: Zero ccache stats and limit in size
	run: ccache -z --max-size=500M
	- name: Perform C/C++ library syntax check
	run: \|
	make -C src/ansi-c library_check
	make -C src/cpp library_check
	- name: Build with make
	run: \|
	make -C src -j${{env.linux-vcpus}} MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical
	make -C unit -j${{env.linux-vcpus}}
	make -C jbmc/src -j${{env.linux-vcpus}}
	make -C jbmc/unit -j${{env.linux-vcpus}}
	- name: Print ccache stats
	run: ccache -s
	- name: Run unit tests
	run: \|
	make -C unit test
	make -C jbmc/unit test
	make TAGS="[z3]" -C unit test
	- name: Run expected failure unit tests
	run: \|
	make TAGS="[!shouldfail]" -C unit test
	make TAGS="[!shouldfail]" -C jbmc/unit test
	- name: Run regression tests
	run: \|
	make -C regression test-parallel JOBS=${{env.linux-vcpus}}
	make -C regression/cbmc test-paths-lifo
	env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2
	make -C jbmc/regression test-parallel JOBS=${{env.linux-vcpus}}

	# This job takes approximately 17 to 41 minutes
	check-ubuntu-22_04-cmake-gcc:
	runs-on: ubuntu-22.04
	steps:
	- uses: actions/checkout@v4
	with:
	submodules: recursive
	- name: Fetch dependencies
	env:
	# This is needed in addition to -yq to prevent apt-get from asking for
	# user input
	DEBIAN_FRONTEND: noninteractive
	run: \|
	sudo apt-get update
	sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc gdb g++ maven flex bison libxml2-utils dpkg-dev ccache doxygen graphviz z3
	- name: Confirm z3 solver is available and log the version installed
	run: z3 --version
	- name: Download cvc-5 from the releases page and make sure it can be deployed
	run: \|
	wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-static.zip
	unzip -j -d /usr/local/bin cvc5-Linux-static.zip cvc5-Linux-static/bin/cvc5
	rm cvc5-Linux-static.zip
	cvc5 --version
	- name: Prepare ccache
	uses: actions/cache@v4
	with:
	save-always: true
	path: .ccache
	key: ${{ runner.os }}-22.04-Release-${{ github.ref }}-${{ github.sha }}-PR
	restore-keys: \|
	${{ runner.os }}-22.04-Release-${{ github.ref }}
	${{ runner.os }}-22.04-Release
	- name: ccache environment
	run: \|
	echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
	echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
	- name: Configure using CMake
	run: cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -Dsat_impl="minisat2;cadical"
	- name: Check that doc task works
	run: ninja -C build doc
	- name: Zero ccache stats and limit in size
	run: ccache -z --max-size=500M
	- name: Build with Ninja
	run: ninja -C build -j${{env.linux-vcpus}}
	- name: Print ccache stats
	run: ccache -s
	- name: Check if package building works
	run: \|
	cd build
	ninja package
	ls *.deb
	- name: Run tests
	run: cd build; ctest . -V -L CORE -j${{env.linux-vcpus}}

	# This job takes approximately 14 to 46 minutes
	check-ubuntu-24_04-cmake-gcc-14:
	runs-on: ubuntu-24.04
	steps:
	- uses: actions/checkout@v4
	with:
	submodules: recursive
	- name: Fetch dependencies
	env:
	# This is needed in addition to -yq to prevent apt-get from asking for
	# user input
	DEBIAN_FRONTEND: noninteractive
	run: \|
	sudo apt-get update
	sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc-14 gdb g++-14 maven flex bison libxml2-utils dpkg-dev ccache doxygen z3
	# Update symlinks so that any use of gcc (including our regression
	# tests) will use GCC 14.
	sudo update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-14 110 \
	--slave /usr/bin/g++ g++ /usr/bin/g++-14 \
	--slave /usr/bin/gcov gcov /usr/bin/gcov-14
	sudo ln -sf cpp-14 /usr/bin/cpp
	- name: Confirm z3 solver is available and log the version installed
	run: z3 --version
	- name: Download cvc-5 from the releases page and make sure it can be deployed
	run: \|
	wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-static.zip
	unzip -j -d /usr/local/bin cvc5-Linux-static.zip cvc5-Linux-static/bin/cvc5
	rm cvc5-Linux-static.zip
	cvc5 --version
	- name: Prepare ccache
	uses: actions/cache@v4
	with:
	save-always: true
	path: .ccache
	key: ${{ runner.os }}-24.04-Release-gcc-14-${{ github.ref }}-${{ github.sha }}-PR
	restore-keys: \|
	${{ runner.os }}-24.04-Release-gcc-14-${{ github.ref }}
	${{ runner.os }}-24.04-Release-gcc-14
	- name: ccache environment
	run: \|
	echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
	echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
	- name: Configure using CMake
	run: cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_CXX_FLAGS=-Wp,-D_GLIBCXX_ASSERTIONS
	- name: Zero ccache stats and limit in size
	run: ccache -z --max-size=500M
	- name: Build with Ninja
	run: ninja -C build -j${{env.linux-vcpus}}
	- name: Print ccache stats
	run: ccache -s
	- name: Run tests
	run: cd build; ctest . -V -L CORE -j${{env.linux-vcpus}}

	# This job takes approximately 14 to 60 minutes
	check-ubuntu-22_04-cmake-gcc-32bit:
	runs-on: ubuntu-22.04
	steps:
	- uses: actions/checkout@v4
	with:
	submodules: recursive
	- name: Fetch dependencies
	env:
	# This is needed in addition to -yq to prevent apt-get from asking for
	# user input
	DEBIAN_FRONTEND: noninteractive
	run: \|
	sudo apt-get update
	sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc gdb g++ maven flex bison libxml2-utils ccache doxygen z3 g++-multilib
	- name: Confirm z3 solver is available and log the version installed
	run: z3 --version
	- name: Download cvc-5 from the releases page and make sure it can be deployed
	run: \|
	wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-static.zip
	unzip -j -d /usr/local/bin cvc5-Linux-static.zip cvc5-Linux-static/bin/cvc5
	rm cvc5-Linux-static.zip
	cvc5 --version
	- name: Prepare ccache
	uses: actions/cache@v4
	with:
	save-always: true
	path: .ccache
	key: ${{ runner.os }}-22.04-Release-32-${{ github.ref }}-${{ github.sha }}-PR
	restore-keys: \|
	${{ runner.os }}-22.04-Release-32-${{ github.ref }}
	${{ runner.os }}-22.04-Release-32
	- name: ccache environment
	run: \|
	echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
	echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
	- name: Configure using CMake
	run: cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -Dsat_impl="minisat2;cadical" -DCMAKE_CXX_FLAGS=-m32
	- name: Zero ccache stats and limit in size
	run: ccache -z --max-size=500M
	- name: Build with Ninja
	run: ninja -C build -j${{env.linux-vcpus}}
	- name: Print ccache stats
	run: ccache -s
	- name: Run tests
	run: cd build; ctest . -V -L CORE -j${{env.linux-vcpus}}

	# This job takes approximately 2 to 24 minutes
	check-ubuntu-20_04-cmake-gcc-KNOWNBUG:
	runs-on: ubuntu-20.04
	steps:
	- uses: actions/checkout@v4
	with:
	submodules: recursive
	- name: Fetch dependencies
	env:
	# This is needed in addition to -yq to prevent apt-get from asking for
	# user input
	DEBIAN_FRONTEND: noninteractive
	run: \|
	sudo apt-get update
	sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc g++ maven flex bison libxml2-utils ccache z3
	- name: Prepare ccache
	uses: actions/cache@v4
	with:
	save-always: true
	path: .ccache
	key: ${{ runner.os }}-20.04-Release-${{ github.ref }}-${{ github.sha }}-PR
	restore-keys: \|
	${{ runner.os }}-20.04-Release-${{ github.ref }}
	${{ runner.os }}-20.04-Release
	- name: ccache environment
	run: \|
	echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
	echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
	- name: Configure using CMake
	run: cmake -H. -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++
	- name: Zero ccache stats and limit in size
	run: ccache -z --max-size=500M
	- name: Build with Ninja
	run: ninja -C build -j${{env.linux-vcpus}}
	- name: Print ccache stats
	run: ccache -s
	- name: Run tests
	run: \|
	cd build
	ctest . -V -L KNOWNBUG -j${{env.linux-vcpus}}
	export PATH=$PWD/bin:$PATH
	cd ../regression/cbmc
	sed -i '1s/^CORE$.$broken-smt-backend/KNOWNBUG\1broken-smt-backend/' /*.desc
	# the following tests fail on Windows only
	git checkout -- memory_allocation1 printf1 printf3 union12 va_list3
	../test.pl -c "cbmc --cprover-smt2" -I broken-smt-backend -K

	# This job takes approximately 7 to 30 minutes
	check-ubuntu-20_04-cmake-gcc-THOROUGH:
	runs-on: ubuntu-20.04
	steps:
	- uses: actions/checkout@v4
	with:
	submodules: recursive
	- name: Fetch dependencies
	env:
	# This is needed in addition to -yq to prevent apt-get from asking for
	# user input
	DEBIAN_FRONTEND: noninteractive
	run: \|
	sudo apt-get update
	sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc g++ maven flex bison libxml2-utils ccache z3
	- name: Prepare ccache
	uses: actions/cache@v4
	with:
	save-always: true
	path: .ccache
	key: ${{ runner.os }}-20.04-Release-${{ github.ref }}-${{ github.sha }}-PR
	restore-keys: \|
	${{ runner.os }}-20.04-Release-${{ github.ref }}
	${{ runner.os }}-20.04-Release
	- name: ccache environment
	run: \|
	echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
	echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
	- name: Configure using CMake
	run: cmake -H. -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -Dsat_impl="minisat2;cadical"
	- name: Zero ccache stats and limit in size
	run: ccache -z --max-size=500M
	- name: Build with Ninja
	run: ninja -C build -j${{env.linux-vcpus}}
	- name: Print ccache stats
	run: ccache -s
	- name: Run tests
	run: cd build; ctest . -V -L THOROUGH -j${{env.linux-vcpus}}

	# This job takes approximately 39 to 69 minutes
	check-macos-13-make-clang:
	runs-on: macos-13
	steps:
	- uses: actions/checkout@v4
	with:
	submodules: recursive
	- name: Fetch dependencies
	run: \|
	# maven is already installed and upgrading to a newer version yields
	# symlink conflicts as previously reported in https://github.com/actions/runner-images/issues/4020
	brew install flex bison parallel ccache z3
	- name: Confirm z3 solver is available and log the version installed
	run: z3 --version
	- name: Download cvc5 binary and make sure it can be deployed
	run: \|
	wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-macOS-static.zip
	unzip -j -d /usr/local/bin cvc5-macOS-static.zip cvc5-macOS-static/bin/cvc5
	rm cvc5-macOS-static.zip
	cvc5 --version
	- name: Prepare ccache
	uses: actions/cache@v4
	with:
	save-always: true
	path: .ccache
	key: ${{ runner.os }}-make-${{ github.ref }}-${{ github.sha }}-PR
	restore-keys: \|
	${{ runner.os }}-make-${{ github.ref }}
	${{ runner.os }}-make
	- name: ccache environment
	run: \|
	echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
	echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
	- name: Zero ccache stats and limit in size
	run: ccache -z --max-size=500M
	- name: Build using Make
	run: \|
	make -C src minisat2-download cadical-download
	make -C src -j4 CXX="ccache clang++" MINISAT2=../../minisat-2.2.1 CADICAL=../../cadical
	make -C jbmc/src -j4 CXX="ccache clang++"
	make -C unit "CXX=ccache clang++"
	make -C jbmc/unit "CXX=ccache clang++"
	- name: Print ccache stats
	run: ccache -s
	- name: Run unit tests
	run: \|
	cd unit; ./unit_tests
	./unit_tests "[z3]"
	- name: Run JBMC unit tests
	run: cd jbmc/unit; ./unit_tests
	- name: Run regression tests
	run: make -C regression test-parallel JOBS=4
	- name: Run JBMC regression tests
	run: make -C jbmc/regression test-parallel JOBS=4

	# This job takes approximately 36 to 85 minutes
	check-macos-14-cmake-clang:
	runs-on: macos-14
	steps:
	- uses: actions/checkout@v4
	with:
	submodules: recursive
	- name: Fetch dependencies
	run: brew install cmake ninja maven flex bison ccache z3
	- name: Confirm z3 solver is available and log the version installed
	run: z3 --version
	- name: Download cvc5 binary and make sure it can be deployed
	run: \|
	wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-macOS-static.zip
	unzip -j -d /usr/local/bin cvc5-macOS-static.zip cvc5-macOS-static/bin/cvc5
	rm cvc5-macOS-static.zip
	cvc5 --version
	- name: Prepare ccache
	uses: actions/cache@v4
	with:
	save-always: true
	path: .ccache
	key: ${{ runner.os }}-Release-${{ github.ref }}-${{ github.sha }}-PR
	restore-keys: \|
	${{ runner.os }}-Release-${{ github.ref }}
	${{ runner.os }}-Release
	- name: ccache environment
	run: \|
	echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
	echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
	- name: Zero ccache stats and limit in size
	run: ccache -z --max-size=500M
	- name: Configure using CMake
	run: \|
	mkdir build
	cd build
	cmake .. -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/clang -DCMAKE_CXX_COMPILER=/usr/bin/clang++ -Dsat_impl=cadical
	- name: Build with Ninja
	run: cd build; ninja -j3
	- name: Print ccache stats
	run: ccache -s
	- name: Run CTest
	run: cd build; ctest -V -L CORE . -j3

	# This job takes approximately 49 to 70 minutes
	check-vs-2019-cmake-build-and-test:
	runs-on: windows-2019
	env:
	GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
	steps:
	- uses: actions/checkout@v4
	with:
	submodules: recursive
	- name: Setup Visual Studio environment
	uses: microsoft/setup-msbuild@v2
	- name: Fetch dependencies
	run: \|
	choco install winflexbison3
	if($LastExitCode -ne 0)
	{
	Write-Output "::error ::Dependency installation via Chocolatey failed."
	exit $LastExitCode
	}
	nuget install clcache -OutputDirectory "c:\tools" -ExcludeVersion -Version 4.1.0
	echo "c:\tools\clcache\clcache-4.1.0" >> $env:GITHUB_PATH
	Invoke-WebRequest -Uri https://github.com/Z3Prover/z3/releases/download/z3-4.8.10/z3-4.8.10-x64-win.zip -OutFile .\z3.zip
	Expand-Archive -LiteralPath '.\z3.Zip' -DestinationPath C:\tools
	echo "c:\tools\z3-4.8.10-x64-win\bin;" >> $env:GITHUB_PATH
	New-Item -ItemType directory "C:\tools\cvc5"
	Invoke-WebRequest -Uri https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Win64-static.zip -OutFile .\cvc5-Win64-static.zip
	Expand-Archive -LiteralPath '.\cvc5-Win64-static.Zip'
	Move-Item -Path .\cvc5-Win64-static\cvc5-Win64-static\bin\cvc5.exe c:\tools\cvc5\cvc5.exe
	echo "c:\tools\cvc5;" >> $env:GITHUB_PATH
	- name: Confirm z3 solver is available and log the version installed
	run: z3 --version
	- name: Confirm cvc5 solver is available and log the version installed
	run: cvc5 --version
	- name: Prepare ccache
	uses: actions/cache@v4
	with:
	save-always: true
	path: .ccache
	key: ${{ runner.os }}-msbuild-${{ github.ref }}-${{ github.sha }}-PR
	restore-keys: \|
	${{ runner.os }}-msbuild-${{ github.ref }}
	${{ runner.os }}-msbuild
	- name: ccache environment
	run: \|
	echo "CLCACHE_BASEDIR=$((Get-Item -Path '.\').FullName)" >> $env:GITHUB_ENV
	echo "CLCACHE_DIR=$pwd\.ccache" >> $env:GITHUB_ENV
	- name: Configure with cmake
	run: cmake -S . -B build
	- name: Zero ccache stats and limit in size (2 GB)
	run: \|
	clcache -z
	clcache -M 2147483648
	- name: Build Release
	run: cmake --build build --config Release -- /p:UseMultiToolTask=true /p:CLToolExe=clcache
	- name: Print ccache stats
	run: clcache -s
	- uses: ilammy/msvc-dev-cmd@v1
	- name: Test cbmc
	run: \|
	Set-Location build
	ctest -V -L CORE -C Release . -j${{env.windows-vcpus}}

	# This job takes approximately 18 to 84 minutes
	check-vs-2022-make-build-and-test:
	runs-on: windows-2022
	env:
	GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
	steps:
	- uses: actions/checkout@v4
	with:
	submodules: recursive
	- name: Setup MSBuild
	uses: microsoft/setup-msbuild@v2
	- name: Fetch dependencies
	run: \|
	choco install -y winflexbison3 strawberryperl wget
	if($LastExitCode -ne 0)
	{
	Write-Output "::error ::Dependency installation via Chocolatey failed."
	exit $LastExitCode
	}
	nuget install clcache -OutputDirectory "c:\tools" -ExcludeVersion -Version 4.1.0
	echo "c:\tools\clcache\clcache-4.1.0" >> $env:GITHUB_PATH
	echo "c:\Strawberry\" >> $env:GITHUB_PATH
	Invoke-WebRequest -Uri https://github.com/Z3Prover/z3/releases/download/z3-4.8.10/z3-4.8.10-x64-win.zip -OutFile .\z3.zip
	Expand-Archive -LiteralPath '.\z3.Zip' -DestinationPath C:\tools
	echo "c:\tools\z3-4.8.10-x64-win\bin;" >> $env:GITHUB_PATH
	New-Item -ItemType directory "C:\tools\cvc5"
	Invoke-WebRequest -Uri https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Win64-static.zip -OutFile .\cvc5-Win64-static.zip
	Expand-Archive -LiteralPath '.\cvc5-Win64-static.Zip'
	Move-Item -Path .\cvc5-Win64-static\cvc5-Win64-static\bin\cvc5.exe c:\tools\cvc5\cvc5.exe
	echo "c:\tools\cvc5;" >> $env:GITHUB_PATH
	New-Item -ItemType directory "C:\tools\parallel"
	wget.exe -O c:\tools\parallel\parallel https://git.savannah.gnu.org/cgit/parallel.git/plain/src/parallel
	echo "c:\tools\parallel" >> $env:GITHUB_PATH
	- name: Confirm z3 solver is available and log the version installed
	run: z3 --version
	- name: Confirm cvc5 solver is available and log the version installed
	run: cvc5 --version
	- name: Initialise Developer Command Line
	uses: ilammy/msvc-dev-cmd@v1
	- name: Prepare ccache
	uses: actions/cache@v4
	with:
	save-always: true
	path: .ccache
	key: ${{ runner.os }}-msbuild-make-${{ github.ref }}-${{ github.sha }}-PR
	restore-keys: \|
	${{ runner.os }}-msbuild-make-${{ github.ref }}
	${{ runner.os }}-msbuild-make
	- name: ccache environment
	run: \|
	echo "CLCACHE_BASEDIR=$((Get-Item -Path '.\').FullName)" >> $env:GITHUB_ENV
	echo "CLCACHE_DIR=$pwd\.ccache" >> $env:GITHUB_ENV
	- name: Zero ccache stats and limit in size (2 GB)
	run: \|
	clcache -z
	clcache -M 2147483648
	- name: Download minisat with make
	run: make -C src minisat2-download
	- name: Build CBMC with make
	run: make CXX=clcache BUILD_ENV=MSVC -j${{env.windows-vcpus}} -C src
	- name: Build unit tests with make
	run: make CXX=clcache BUILD_ENV=MSVC -j${{env.windows-vcpus}} -C unit all
	- name: Build jbmc with make
	run: \|
	make CXX=clcache -j${{env.windows-vcpus}} -C jbmc/src setup-submodules
	make CXX=clcache BUILD_ENV=MSVC -j${{env.windows-vcpus}} -C jbmc/src
	- name: Build JBMC unit tests
	run: make CXX=clcache BUILD_ENV=MSVC -j${{env.windows-vcpus}} -C jbmc/unit all
	- name: Print ccache stats
	run: clcache -s
	- name: Run CBMC and JBMC unit tests
	run: \|
	make CXX=clcache BUILD_ENV=MSVC -C unit test
	make CXX=clcache BUILD_ENV=MSVC -C unit test TAGS="[z3]"
	make CXX=clcache BUILD_ENV=MSVC -C jbmc/unit test
	- name: Run CBMC regression tests
	run: make CXX=clcache BUILD_ENV=MSVC -C regression test-parallel JOBS=${{env.windows-vcpus}}

	# This job takes approximately 7 to 32 minutes
	windows-msi-package:
	runs-on: windows-2019
	env:
	GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
	steps:
	- uses: actions/checkout@v4
	with:
	submodules: recursive
	- name: Setup Visual Studio environment
	uses: microsoft/setup-msbuild@v2
	- name: Fetch dependencies
	run: \|
	choco install winflexbison3
	if($LastExitCode -ne 0)
	{
	Write-Output "::error ::Dependency installation via Chocolatey failed."
	exit $LastExitCode
	}
	nuget install clcache -OutputDirectory "c:\tools" -ExcludeVersion -Version 4.1.0
	echo "c:\tools\clcache\clcache-4.1.0" >> $env:GITHUB_PATH
	- name: Prepare ccache
	uses: actions/cache@v4
	with:
	save-always: true
	path: .ccache
	key: ${{ runner.os }}-msbuild-${{ github.ref }}-${{ github.sha }}-PKG
	restore-keys: \|
	${{ runner.os }}-msbuild-${{ github.ref }}
	${{ runner.os }}-msbuild
	- name: ccache environment
	run: \|
	echo "CLCACHE_BASEDIR=$((Get-Item -Path '.\').FullName)" >> $env:GITHUB_ENV
	echo "CLCACHE_DIR=$pwd\.ccache" >> $env:GITHUB_ENV
	- name: Configure with cmake
	run: cmake -S . -B build
	- name: Build Release
	run: cmake --build build --config Release -- /p:UseMultiToolTask=true /p:CLToolExe=clcache
	- name: Print ccache stats
	run: clcache -s
	- name: Create packages
	id: create_packages
	# We need to get the path to cpack because fascinatingly,
	# chocolatey also includes a command called "cpack" which takes precedence
	run: \|
	Set-Location build
	$cpack = "$(Split-Path -Parent (Get-Command cmake).Source)\cpack.exe"
	& $cpack . -C Release
	$msi_name = (Get-ChildItem -name *.msi).Name
	echo "msi_installer=build/$msi_name" >> $env:GITHUB_OUTPUT
	echo "msi_name=$msi_name" >> $env:GITHUB_OUTPUT

	# This job takes approximately 2 to 3 minutes
	check-string-table:
	runs-on: ubuntu-20.04
	steps:
	- uses: actions/checkout@v4
	- name: Check for unused irep ids
	run: ./scripts/string_table_check.sh

	# This job takes approximately 23 to 29 minutes
	check-docker-image:
	runs-on: ubuntu-20.04
	steps:
	- uses: actions/checkout@v4
	with:
	submodules: recursive
	- name: Download test dependencies
	run: \|
	sudo apt update
	sudo apt install openjdk-11-jdk-headless
	- name: Build docker image
	run: docker build -t cbmc .
	- name: Smoke test goto-cc
	run: docker run -v ${PWD}/.github/workflows/smoke_test_assets:/mnt/smoke -t cbmc goto-cc -o /mnt/smoke/test.goto /mnt/smoke/test.c
	- name: Smoke test cbmc
	run: docker run -v ${PWD}/.github/workflows/smoke_test_assets:/mnt/smoke -t cbmc cbmc /mnt/smoke/test.goto
	- name: Smoke test jbmc
	run: \|
	javac .github/workflows/smoke_test_assets/Test.java
	docker run -v ${PWD}/.github/workflows/smoke_test_assets:/mnt/smoke -t cbmc jbmc --classpath /mnt/smoke Test
	- name: Smoke test goto-analyzer
	run: docker run -v ${PWD}/.github/workflows/smoke_test_assets:/mnt/smoke -t cbmc goto-analyzer /mnt/smoke/test.goto --unreachable-functions

	# This job takes approximately 22 to 41 minutes
	include-what-you-use:
	runs-on: ubuntu-22.04
	steps:
	- uses: actions/checkout@v4
	with:
	submodules: recursive
	- name: Fetch dependencies
	env:
	# This is needed in addition to -yq to prevent apt-get from asking for
	# user input
	DEBIAN_FRONTEND: noninteractive
	run: \|
	sudo apt-get update
	sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc gdb g++ maven flex bison iwyu
	- name: Configure using CMake
	run: cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++
	- name: Run include-what-you-use
	run: \|
	iwyu_tool -p build/compile_commands.json -j${{env.linux-vcpus}} \| tee includes.txt
	if sed '/minisat2-src/,/^--$/d' includes.txt \| grep '^- ' -B1 ; then
	echo "Unnecessary includes found. Use '// IWYU pragma: keep' to override this."
	exit 1
	fi

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

CONTRACTS: add doc for loop assigns inference #10600

Workflow file

CONTRACTS: add doc for loop assigns inference #10600

Jobs

Run details

Workflow file for this run