|
59 | 59 | env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2
|
60 | 60 | make -C jbmc/regression test-parallel JOBS=2
|
61 | 61 |
|
| 62 | + check-ubuntu-20_04-make-clang: |
| 63 | + runs-on: ubuntu-20.04 |
| 64 | + env: |
| 65 | + CC: "ccache /usr/bin/clang" |
| 66 | + CXX: "ccache /usr/bin/clang++" |
| 67 | + steps: |
| 68 | + - uses: actions/checkout@v2 |
| 69 | + with: |
| 70 | + submodules: recursive |
| 71 | + - name: Fetch dependencies |
| 72 | + env: |
| 73 | + # This is needed in addition to -yq to prevent apt-get from asking for |
| 74 | + # user input |
| 75 | + DEBIAN_FRONTEND: noninteractive |
| 76 | + run: | |
| 77 | + sudo apt-get update |
| 78 | + sudo apt-get install --no-install-recommends -yq clang-10 clang++-10 gdb maven jq flex bison libxml2-utils cpanminus ccache |
| 79 | + make -C src minisat2-download |
| 80 | + cpanm Thread::Pool::Simple |
| 81 | + - name: Prepare ccache |
| 82 | + uses: actions/cache@v2 |
| 83 | + with: |
| 84 | + path: .ccache |
| 85 | + key: ${{ runner.os }}-20.04-make-clang-${{ github.ref }}-${{ github.sha }}-PR |
| 86 | + restore-keys: | |
| 87 | + ${{ runner.os }}-20.04-make-clang-${{ github.ref }} |
| 88 | + ${{ runner.os }}-20.04-make-clang |
| 89 | + - name: ccache environment |
| 90 | + run: | |
| 91 | + echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV |
| 92 | + echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV |
| 93 | + - name: Zero ccache stats and limit in size |
| 94 | + run: ccache -z --max-size=500M |
| 95 | + - name: Build with make |
| 96 | + run: | |
| 97 | + make -C src -j2 |
| 98 | + make -C unit -j2 |
| 99 | + make -C jbmc/src -j2 |
| 100 | + make -C jbmc/unit -j2 |
| 101 | + - name: Print ccache stats |
| 102 | + run: ccache -s |
| 103 | + - name: Run unit tests |
| 104 | + run: | |
| 105 | + make -C unit test |
| 106 | + make -C jbmc/unit test |
| 107 | + - name: Run expected failure unit tests |
| 108 | + run: | |
| 109 | + make TAGS="[!shouldfail]" -C unit test |
| 110 | + make TAGS="[!shouldfail]" -C jbmc/unit test |
| 111 | + - name: Run regression tests |
| 112 | + run: | |
| 113 | + make -C regression test-parallel JOBS=2 |
| 114 | + make -C regression/cbmc test-paths-lifo |
| 115 | + env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2 |
| 116 | + make -C jbmc/regression test-parallel JOBS=2 |
| 117 | +
|
62 | 118 | check-ubuntu-20_04-cmake-gcc:
|
63 | 119 | runs-on: ubuntu-20.04
|
64 | 120 | steps:
|
|
0 commit comments