CONTRACTS: add doc for loop assigns inference #1327
Workflow file for this run
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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 |