add tests for SMV LTLSPEC #2494

Workflow file for this run

.github/workflows/pull-request-checks.yaml at 5e0476b

	name: Build and Test HW-CBMC
	on:
	push:
	branches: [ main ]
	pull_request:
	branches: [ main ]

	jobs:
	# This job takes approximately 15 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++ jq flex bison libxml2-utils ccache cmake z3
	- name: Confirm z3 solver is available and log the version installed
	run: z3 --version
	- name: Prepare ccache
	uses: actions/cache@v4
	with:
	path: .ccache
	save-always: true
	key: ${{ runner.os }}-20.04-make-gcc-${{ github.ref }}-${{ github.sha }}-PR
	restore-keys: \|
	${{ runner.os }}-20.04-make-gcc-${{ github.ref }}
	${{ runner.os }}-20.04-make-gcc
	- 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: Get minisat
	run: \|
	make -C lib/cbmc/src minisat2-download
	- name: Build with make
	run: make -C src -j4 CXX="ccache g++"
	- name: Run the ebmc tests with SAT
	run: make -C regression/ebmc test
	- name: Run the ebmc tests with Z3
	run: make -C regression/ebmc test-z3
	- name: Run the verilog tests
	run: make -C regression/verilog test
	- name: Run the verilog tests with Z3
	run: make -C regression/verilog test-z3
	- name: Run the vlindex tests
	run: make -C regression/vlindex test
	- name: Print ccache stats
	run: ccache -s

	# This job takes approximately 15 minutes
	check-ubuntu-20_04-make-clang:
	runs-on: ubuntu-20.04
	env:
	CC: "ccache clang"
	CXX: "ccache 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 jq flex bison libxml2-utils cpanminus ccache z3
	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:
	path: .ccache
	save-always: true
	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: Get minisat
	run: \|
	make -C lib/cbmc/src minisat2-download
	- name: Build with make
	run: make CXX="ccache clang++" -C src -j4
	- name: Run the ebmc tests with SAT
	run: make -C regression/ebmc test
	- name: Run the ebmc tests with Z3
	run: make -C regression/ebmc test-z3
	- name: Run the verilog tests
	run: make -C regression/verilog test
	- name: Run the verilog tests with Z3
	run: make -C regression/verilog test-z3
	- name: Run the vlindex tests
	run: make -C regression/vlindex test
	- name: Print ccache stats
	run: ccache -s
	- name: Upload the ebmc binary
	uses: actions/upload-artifact@v4
	with:
	name: ebmc-binary
	retention-days: 5
	path: src/ebmc/ebmc

	# This job takes approximately 4 minutes
	benchmarking:
	runs-on: ubuntu-20.04
	needs: check-ubuntu-20_04-make-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 z3
	- name: Confirm z3 solver is available and log the version installed
	run: z3 --version
	- name: Get the ebmc binary
	uses: actions/download-artifact@v4
	with:
	name: ebmc-binary
	path: ebmc
	- name: Try the ebmc binary
	run: chmod a+x ./ebmc/ebmc ; ./ebmc/ebmc --version
	- name: HWMCC08 benchmarks
	run: PATH=$PATH:$PWD/ebmc benchmarking/hwmcc08.sh

	# This job takes approximately 15 minutes
	check-centos8-make-gcc:
	name: CentOS 8
	runs-on: ubuntu-22.04
	container:
	image: centos:8
	steps:
	- name: Install Packages
	run: \|
	sed -i -e "s\|mirrorlist=\|#mirrorlist=\|g" -e "s\|#baseurl=http://mirror.centos.org\|baseurl=http://vault.centos.org\|g" /etc/yum.repos.d/CentOS-Linux-*
	yum -y install make gcc-c++ flex bison git rpmdevtools wget
	wget --no-verbose https://github.com/ccache/ccache/releases/download/v4.8.3/ccache-4.8.3-linux-x86_64.tar.xz
	tar xJf ccache-4.8.3-linux-x86_64.tar.xz
	cp ccache-4.8.3-linux-x86_64/ccache /usr/bin/
	# yum install dnf-plugins-core
	# yum config-manager --set-enabled powertools
	# yum install glibc-static libstdc++-static
	- name: cache for ccache
	uses: actions/cache@v4
	with:
	path: /github/home/.cache/ccache
	save-always: true
	key: ${{ runner.os }}-centos8-make-gcc-${{ github.ref }}-${{ github.sha }}-PR
	restore-keys: ${{ runner.os }}-centos8-make-gcc-
	- uses: actions/checkout@v4
	with:
	submodules: recursive
	- name: Zero ccache stats and limit in size
	run: ccache -z --max-size=500M
	- name: ccache path
	run: ccache -p \| grep cache_dir
	- name: Get minisat
	run: make -C lib/cbmc/src minisat2-download
	- name: Build with make
	run: make CXX="ccache g++ -Wno-class-memaccess" LIBS="-lstdc++fs" -C src -j4
	- name: Run the ebmc tests with SAT
	run: \|
	rm regression/ebmc/neural-liveness/counter1.desc
	make -C regression/ebmc test
	- name: Run the verilog tests
	run: make -C regression/verilog test
	- name: Run the vlindex tests
	run: make -C regression/vlindex test
	- name: Print ccache stats
	run: ccache -s

	# This job takes approximately 20 minutes
	check-macos-14-make-clang:
	runs-on: macos-14
	steps:
	- uses: actions/checkout@v4
	with:
	submodules: recursive
	- name: Fetch dependencies
	run: brew install bison ccache z3
	- 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 }}-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: Get minisat
	run: make -C lib/cbmc/src minisat2-download
	- name: Build with make
	run: make YACC="/opt/homebrew/opt/bison/bin/bison" CXX="ccache clang++" -C src -j3
	- name: Run the ebmc tests with SAT
	run: make -C regression/ebmc test
	- name: Run the ebmc tests with Z3
	run: make -C regression/ebmc test-z3
	- name: Run the verilog tests
	run: make -C regression/verilog test
	- name: Run the verilog tests with Z3
	run: make -C regression/verilog test-z3
	- name: Run the vlindex tests
	run: make -C regression/vlindex test
	- name: Print ccache stats
	run: ccache -s

	# This job takes approximately 17 minutes
	check-ubuntu-24_04-make-emcc:
	name: Emscripten build
	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 emscripten flex bison libxml2-utils cpanminus ccache
	- name: Prepare ccache
	uses: actions/cache@v4
	with:
	path: .ccache
	save-always: true
	key: ${{ runner.os }}-24.04-make-emcc-${{ github.ref }}-${{ github.sha }}-PR
	restore-keys: \|
	${{ runner.os }}-24.04-make-emcc-${{ github.ref }}
	${{ runner.os }}-24.04-make-emcc
	- 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: Get minisat
	run: make -C lib/cbmc/src minisat2-download
	- name: Build with make
	run: make -C src -j4 CXX="ccache emcc" HOSTCXX="ccache g++" BUILD_ENV=Unix LINKLIB="emar rc \$@ \$^" AR="emar" EXEEXT=".html"
	- name: print version number via node.js
	run: node --no-experimental-fetch src/ebmc/ebmc.js --version
	- name: Print ccache stats
	run: ccache -s

	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 --no-progress 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\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: 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 lib/cbmc/src minisat2-download
	- name: Build EBMC with make
	env:
	# disable MSYS file-name mangling
	MSYS2_ARG_CONV_EXCL: "*"
	run: make CXX=clcache BUILD_ENV=MSVC -j4 -C src
	- name: Print ccache stats
	run: clcache -s

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

add tests for SMV LTLSPEC #2494

Workflow file

add tests for SMV LTLSPEC #2494

Jobs

Run details

Workflow file for this run