-
Notifications
You must be signed in to change notification settings - Fork 269
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Uses the same virtualisation set-up as FreeBSD checks.
- Loading branch information
1 parent
7b06901
commit 042bf99
Showing
1 changed file
with
110 additions
and
0 deletions.
There are no files selected for viewing
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -60,3 +60,113 @@ jobs: | |
| 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=3 | ||
| # This job takes approximately X to Y minutes | ||
| openbsd: | ||
| runs-on: macos-12 | ||
| steps: | ||
| - uses: actions/checkout@v3 | ||
| with: | ||
| submodules: recursive | ||
| - name: Prepare ccache | ||
| uses: actions/cache@v3 | ||
| with: | ||
| 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: cross-platform-actions/[email protected] | ||
| with: | ||
| operating_system: openbsd | ||
| version: '7.4' | ||
| run: | | ||
| echo "Fetch dependencies" | ||
| sudo pkg install -y bash gmake git www/p5-libwww python python3 patch flex bison ccache parallel cvc5 z3 | ||
| echo "Fetch JBMC dependencies" | ||
| sudo pkg install -y openjdk8 wget maven | ||
| echo "Zero ccache stats and limit in size" | ||
| ccache -z --max-size=500M | ||
| echo "Build with gmake" | ||
| # don't do JBMC as to keep the overall time in check | ||
| gmake -C src minisat2-download | ||
| gmake -C src -j3 CXX="ccache clang++" | ||
| # gmake -C jbmc/src setup-submodules | ||
| # gmake -C jbmc/src -j3 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 test-parallel JOBS=3 | ||
| 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=3 | ||
| # This job takes approximately X to Y minutes | ||
| netbsd: | ||
| runs-on: macos-12 | ||
| steps: | ||
| - uses: actions/checkout@v3 | ||
| with: | ||
| submodules: recursive | ||
| - name: Prepare ccache | ||
| uses: actions/cache@v3 | ||
| with: | ||
| 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: cross-platform-actions/[email protected] | ||
| with: | ||
| operating_system: netbsd | ||
| version: '9.3' | ||
| run: | | ||
| echo "Fetch dependencies" | ||
| sudo pkg install -y bash gmake git www/p5-libwww python python3 patch flex bison ccache parallel cvc5 z3 | ||
| echo "Fetch JBMC dependencies" | ||
| sudo pkg install -y openjdk8 wget maven | ||
| echo "Zero ccache stats and limit in size" | ||
| ccache -z --max-size=500M | ||
| echo "Build with gmake" | ||
| # don't do JBMC as to keep the overall time in check | ||
| gmake -C src minisat2-download | ||
| gmake -C src -j3 CXX="ccache clang++" | ||
| # gmake -C jbmc/src setup-submodules | ||
| # gmake -C jbmc/src -j3 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 test-parallel JOBS=3 | ||
| 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=3 | ||