|
40 | 40 | env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2
|
41 | 41 | make -C jbmc/regression test
|
42 | 42 |
|
| 43 | + check-ubuntu-20_04-make-clang: |
| 44 | + runs-on: ubuntu-20.04 |
| 45 | + steps: |
| 46 | + - uses: actions/checkout@v2 |
| 47 | + with: |
| 48 | + submodules: true |
| 49 | + - name: Fetch dependencies |
| 50 | + env: |
| 51 | + # This is needed in addition to -yq to prevent apt-get from asking for |
| 52 | + # user input |
| 53 | + DEBIAN_FRONTEND: noninteractive |
| 54 | + TESTPL_JOBS: 4 |
| 55 | + run: | |
| 56 | + sudo apt-get install -yq gdb maven jq flex bison libxml2-utils cpanminus |
| 57 | + make -C src minisat2-download |
| 58 | + cpanm Thread::Pool::Simple |
| 59 | + - name: Build with make |
| 60 | + run: | |
| 61 | + make -C src CXX='/usr/bin/clang++' -j2 |
| 62 | + make -C unit CXX='/usr/bin/clang++' -j2 |
| 63 | + make -C jbmc/src CXX='/usr/bin/clang++' -j2 |
| 64 | + make -C jbmc/unit CXX='/usr/bin/clang++' -j2 |
| 65 | + - name: Run unit tests |
| 66 | + run: | |
| 67 | + make -C unit CXX='/usr/bin/clang++' test |
| 68 | + make -C jbmc/unit CXX='/usr/bin/clang++' test |
| 69 | + echo "Running expected failure tests" |
| 70 | + make TAGS="[!shouldfail]" -C unit CXX='/usr/bin/clang++' test |
| 71 | + make TAGS="[!shouldfail]" -C jbmc/unit CXX='/usr/bin/clang++' test |
| 72 | + - name: Run regression tests |
| 73 | + run: | |
| 74 | + make -C regression test |
| 75 | + make -C regression/cbmc test-paths-lifo |
| 76 | + env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2 |
| 77 | + make -C jbmc/regression test |
| 78 | +
|
43 | 79 | check-ubuntu-20_04-cmake-gcc:
|
44 | 80 | runs-on: ubuntu-20.04
|
45 | 81 | steps:
|
|
0 commit comments