Skip to content

[CONTRACTS] Use fresh converter in loop contracts instrumentation #727

[CONTRACTS] Use fresh converter in loop contracts instrumentation

[CONTRACTS] Use fresh converter in loop contracts instrumentation #727

Workflow file for this run

name: Build and Test on *BSD
on:
push:
branches: [ develop ]
pull_request:
branches: [ develop ]
jobs:
# This job takes approximately 6 to 26 minutes
FreeBSD:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
with:
submodules: recursive
- name: Prepare ccache
uses: actions/cache@v4
with:
save-always: true
path: .ccache
key: freebsd-13.2-gmake-${{ github.ref }}-${{ github.sha }}-PR
restore-keys: |
freebsd-13.2-gmake-${{ github.ref }}
freebsd-13.2-gmake
- name: ccache environment
run: |
echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
- name: Build and Test
uses: vmactions/freebsd-vm@v1
with:
release: 13.2
usesh: true
run: |
# apparently fail-on-error isn't the default here
set -e -x
echo "Fetch dependencies"
pkg install -y bash gmake git www/p5-libwww python python3 patch flex bison ccache parallel cvc5 z3
echo "Fetch JBMC dependencies"
pkg install -y openjdk8 wget maven
echo "Zero ccache stats and limit in size"
export CCACHE_BASEDIR=$PWD
export CCACHE_DIR=$PWD/.ccache
ccache -z --max-size=500M
ccache -p
echo "Build with gmake"
# don't do JBMC as to keep the overall time in check
gmake -C src minisat2-download
gmake -C src -j2 CXX="ccache clang++"
# gmake -C jbmc/src setup-submodules
# gmake -C jbmc/src -j2 CXX="ccache clang++"
gmake -C unit "CXX=ccache clang++"
# gmake -C jbmc/unit "CXX=ccache clang++"
echo "Print ccache stats"
ccache -s
echo "Checking completeness of help output"
scripts/check_help.sh clang++
echo "Run unit tests"
gmake -C unit test
# gmake -C jbmc/unit test
echo "Running expected failure tests"
gmake TAGS='[!shouldfail]' -C unit test
# gmake TAGS='[!shouldfail]' -C jbmc/unit test
echo "Run regression tests"
gmake -C regression/cbmc test
# gmake -C regression test-parallel JOBS=2
# gmake -C regression/cbmc test-paths-lifo
# env PATH=$PATH:`pwd`/src/solvers gmake -C regression/cbmc test-cprover-smt2
# # gmake -C jbmc/regression test-parallel JOBS=2
# This job takes approximately 7 to 34 minutes
OpenBSD:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
with:
submodules: recursive
- name: Prepare ccache
uses: actions/cache@v4
with:
save-always: true
path: .ccache
key: openbsd-7.4-gmake-${{ github.ref }}-${{ github.sha }}-PR
restore-keys: |
openbsd-7.4-gmake-${{ github.ref }}
openbsd-7.4-gmake
- name: ccache environment
run: |
echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
- name: Build and Test
uses: vmactions/openbsd-vm@v1
with:
release: 7.4
run: |
# apparently fail-on-error isn't the default here
set -e -x
echo "Fetch dependencies"
pkg_add -v bash gmake llvm%16 git python3 bison ccache parallel z3
ln -s $(which llvm-ar-16) /usr/local/bin/llvm-ar
echo "Fetch JBMC dependencies"
pkg_add -v jdk%1.8 wget maven
echo "Zero ccache stats and limit in size"
export CCACHE_BASEDIR=$PWD
export CCACHE_DIR=$PWD/.ccache
ccache -z --max-size=500M
ccache -p
echo "Build with gmake"
# don't do JBMC so as to keep the overall time in check
gmake -C src minisat2-download
gmake -C src -j2 CXX="ccache clang++"
# gmake -C jbmc/src setup-submodules
# gmake -C jbmc/src -j2 CXX="ccache clang++"
gmake -C unit "CXX=ccache clang++"
# gmake -C jbmc/unit "CXX=ccache clang++"
echo "Print ccache stats"
ccache -s
echo "Checking completeness of help output"
scripts/check_help.sh clang++
echo "Run unit tests"
gmake -C unit test
# gmake -C jbmc/unit test
echo "Running expected failure tests"
gmake TAGS='[!shouldfail]' -C unit test
# gmake TAGS='[!shouldfail]' -C jbmc/unit test
echo "Run regression tests"
gmake -C regression/cbmc test
# gmake -C regression test-parallel JOBS=2
# gmake -C regression/cbmc test-paths-lifo
# env PATH=$PATH:`pwd`/src/solvers gmake -C regression/cbmc test-cprover-smt2
# # gmake -C jbmc/regression test-parallel JOBS=2
# This job takes approximately 6 to 29 minutes
NetBSD:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
with:
submodules: recursive
- name: Prepare ccache
uses: actions/cache@v4
with:
save-always: true
path: .ccache
key: netbsd-9.3-gmake-${{ github.ref }}-${{ github.sha }}-PR
restore-keys: |
netbsd-9.3-gmake-${{ github.ref }}
netbsd-9.3-gmake
- name: ccache environment
run: |
echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
- name: Build and Test
uses: vmactions/netbsd-vm@v1
with:
release: 9.3
run: |
# apparently fail-on-error isn't the default here
set -e -x
echo "Fetch dependencies"
pkg_add -v bash gmake git python311 patch flex bison ccache parallel z3 gcc10
ln -s $(which python3.11) /usr/pkg/bin/python3
export PATH=/usr/pkg/gcc10/bin:$PATH
echo "Fetch JBMC dependencies"
pkg_add -v openjdk8 wget apache-maven
echo "Zero ccache stats and limit in size"
export CCACHE_BASEDIR=$PWD
export CCACHE_DIR=$PWD/.ccache
ccache -z --max-size=500M
ccache -p
echo "Build with gmake"
# don't do JBMC so as to keep the overall time in check
gmake -C src minisat2-download
gmake -C src -j2 CXX="ccache g++"
# gmake -C jbmc/src setup-submodules
# gmake -C jbmc/src -j2 CXX="ccache g++"
gmake -C unit "CXX=ccache g++"
# gmake -C jbmc/unit "CXX=ccache g++"
echo "Print ccache stats"
ccache -s
echo "Checking completeness of help output"
scripts/check_help.sh g++
echo "Run unit tests"
# TODO: unit tests are failing, requires debugging
gmake -C unit test || true
# gmake -C jbmc/unit test
echo "Running expected failure tests"
gmake TAGS='[!shouldfail]' -C unit test
# gmake TAGS='[!shouldfail]' -C jbmc/unit test
echo "Run regression tests"
# TODO: we need to model some more library functions
gmake -C regression/cbmc test || true
# gmake -C regression test-parallel JOBS=2
# gmake -C regression/cbmc test-paths-lifo
# env PATH=$PATH:`pwd`/src/solvers gmake -C regression/cbmc test-cprover-smt2
# # gmake -C jbmc/regression test-parallel JOBS=2