Skip to content

Commit ab0071c

Browse files
committed
Run KNOWNBUG and THOROUGH regression tests in CI
Copy the check-ubuntu-20_04-cmake-gcc job to run KNOWNBUG (any test reported as failure will tell us that a bug has unexpectedly been fixed) an THOROUGH (tests that are expected to pass, but take longer to do so) tests, each as a separate GitHub action. Also run all tests tagged broken-smt-backend to confirm they haven't been fixed.
1 parent 1d3f2f2 commit ab0071c

File tree

1 file changed

+88
-0
lines changed

1 file changed

+88
-0
lines changed

.github/workflows/pull-request-checks.yaml

Lines changed: 88 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -170,6 +170,94 @@ jobs:
170170
- name: Run tests
171171
run: cd build; ctest . -V -L CORE -j2
172172

173+
check-ubuntu-20_04-cmake-gcc-KNOWNBUG:
174+
runs-on: ubuntu-20.04
175+
steps:
176+
- uses: actions/checkout@v2
177+
with:
178+
submodules: recursive
179+
- name: Fetch dependencies
180+
env:
181+
# This is needed in addition to -yq to prevent apt-get from asking for
182+
# user input
183+
DEBIAN_FRONTEND: noninteractive
184+
run: |
185+
sudo apt-get update
186+
sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc g++ maven flex bison libxml2-utils ccache z3
187+
- name: Confirm z3 solver is available and log the version installed
188+
run: z3 --version
189+
- name: Prepare ccache
190+
uses: actions/cache@v2
191+
with:
192+
path: .ccache
193+
key: ${{ runner.os }}-20.04-Release-${{ github.ref }}-${{ github.sha }}-PR
194+
restore-keys: |
195+
${{ runner.os }}-20.04-Release-${{ github.ref }}
196+
${{ runner.os }}-20.04-Release
197+
- name: ccache environment
198+
run: |
199+
echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
200+
echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
201+
- name: Configure using CMake
202+
run: cmake -H. -Bbuild -G Ninja
203+
- name: Zero ccache stats and limit in size
204+
run: ccache -z --max-size=500M
205+
- name: Build with Ninja
206+
run: ninja -C build -j2
207+
- name: Print ccache stats
208+
run: ccache -s
209+
- name: Run tests
210+
run: |
211+
cd build
212+
ctest . -V -L KNOWNBUG -j2
213+
export PATH=$PWD/bin:$PATH
214+
cd ../regression/cbmc
215+
sed -i '1s/^CORE\(.*\)broken-smt-backend/KNOWNBUG\1broken-smt-backend/' */*.desc
216+
# the following tests fail on Windows only
217+
git checkout -- memory_allocation1 printf1 union12 va_list3
218+
# the following tests fail on Ubuntu 18.04 only
219+
git checkout -- byte_update12 gcc_vector1
220+
../test.pl -c "cbmc --cprover-smt2" -I broken-smt-backend -K
221+
222+
check-ubuntu-20_04-cmake-gcc-THOROUGH:
223+
runs-on: ubuntu-20.04
224+
steps:
225+
- uses: actions/checkout@v2
226+
with:
227+
submodules: recursive
228+
- name: Fetch dependencies
229+
env:
230+
# This is needed in addition to -yq to prevent apt-get from asking for
231+
# user input
232+
DEBIAN_FRONTEND: noninteractive
233+
run: |
234+
sudo apt-get update
235+
sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc g++ maven flex bison libxml2-utils ccache z3
236+
- name: Confirm z3 solver is available and log the version installed
237+
run: z3 --version
238+
- name: Prepare ccache
239+
uses: actions/cache@v2
240+
with:
241+
path: .ccache
242+
key: ${{ runner.os }}-20.04-Release-${{ github.ref }}-${{ github.sha }}-PR
243+
restore-keys: |
244+
${{ runner.os }}-20.04-Release-${{ github.ref }}
245+
${{ runner.os }}-20.04-Release
246+
- name: ccache environment
247+
run: |
248+
echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
249+
echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
250+
- name: Configure using CMake
251+
run: cmake -H. -Bbuild -G Ninja
252+
- name: Zero ccache stats and limit in size
253+
run: ccache -z --max-size=500M
254+
- name: Build with Ninja
255+
run: ninja -C build -j2
256+
- name: Print ccache stats
257+
run: ccache -s
258+
- name: Run tests
259+
run: cd build; ctest . -V -L THOROUGH -j2
260+
173261
check-macos-10_15-make-clang:
174262
runs-on: macos-10.15
175263
steps:

0 commit comments

Comments
 (0)