Skip to content

Commit ffd4ccf

Browse files
tautschnigtautschnig
authored
Merge pull request #5958 from tautschnig/test-thorough
Run KNOWNBUG and THOROUGH regression tests in CI
2 parents 84ad287 + 882c670 commit ffd4ccf

File tree

878 files changed

+971
-886
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

878 files changed

+971
-886
lines changed

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

Lines changed: 84 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -170,6 +170,90 @@ 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: Prepare ccache
188+
uses: actions/cache@v2
189+
with:
190+
path: .ccache
191+
key: ${{ runner.os }}-20.04-Release-${{ github.ref }}-${{ github.sha }}-PR
192+
restore-keys: |
193+
${{ runner.os }}-20.04-Release-${{ github.ref }}
194+
${{ runner.os }}-20.04-Release
195+
- name: ccache environment
196+
run: |
197+
echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
198+
echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
199+
- name: Configure using CMake
200+
run: cmake -H. -Bbuild -G Ninja
201+
- name: Zero ccache stats and limit in size
202+
run: ccache -z --max-size=500M
203+
- name: Build with Ninja
204+
run: ninja -C build -j2
205+
- name: Print ccache stats
206+
run: ccache -s
207+
- name: Run tests
208+
run: |
209+
cd build
210+
ctest . -V -L KNOWNBUG -j2
211+
export PATH=$PWD/bin:$PATH
212+
cd ../regression/cbmc
213+
sed -i '1s/^CORE\(.*\)broken-smt-backend/KNOWNBUG\1broken-smt-backend/' */*.desc
214+
# the following test fails on some Unix systems
215+
git checkout -- r_w_ok6
216+
# the following tests fail on Windows only
217+
git checkout -- memory_allocation1 printf1 union12 va_list3
218+
../test.pl -c "cbmc --cprover-smt2" -I broken-smt-backend -K
219+
220+
check-ubuntu-20_04-cmake-gcc-THOROUGH:
221+
runs-on: ubuntu-20.04
222+
steps:
223+
- uses: actions/checkout@v2
224+
with:
225+
submodules: recursive
226+
- name: Fetch dependencies
227+
env:
228+
# This is needed in addition to -yq to prevent apt-get from asking for
229+
# user input
230+
DEBIAN_FRONTEND: noninteractive
231+
run: |
232+
sudo apt-get update
233+
sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc g++ maven flex bison libxml2-utils ccache z3
234+
- name: Prepare ccache
235+
uses: actions/cache@v2
236+
with:
237+
path: .ccache
238+
key: ${{ runner.os }}-20.04-Release-${{ github.ref }}-${{ github.sha }}-PR
239+
restore-keys: |
240+
${{ runner.os }}-20.04-Release-${{ github.ref }}
241+
${{ runner.os }}-20.04-Release
242+
- name: ccache environment
243+
run: |
244+
echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
245+
echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
246+
- name: Configure using CMake
247+
run: cmake -H. -Bbuild -G Ninja
248+
- name: Zero ccache stats and limit in size
249+
run: ccache -z --max-size=500M
250+
- name: Build with Ninja
251+
run: ninja -C build -j2
252+
- name: Print ccache stats
253+
run: ccache -s
254+
- name: Run tests
255+
run: cd build; ctest . -V -L THOROUGH -j2
256+
173257
check-macos-10_15-make-clang:
174258
runs-on: macos-10.15
175259
steps:

‎jbmc/regression/jbmc-strings/VerifStringLastIndexOf/Test.class

322 Bytes
Binary file not shown.

‎jbmc/regression/jbmc-strings/VerifStringLastIndexOf/Test.java

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,8 @@ public int referenceLastIndexOf(String s, char ch, int fromIndex) {
1919
}
2020

2121
public int check(String s, char ch, int fromIndex) {
22+
if(s.length() <= fromIndex)
23+
return -1;
2224
int reference = referenceLastIndexOf(s, ch, fromIndex);
2325
int jbmc_result = s.lastIndexOf(ch, fromIndex);
2426
assert(reference == jbmc_result);

‎jbmc/regression/jbmc-strings/VerifStringLastIndexOf/test.desc

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
11
THOROUGH
22
Test
3-
--function Test.check --max-nondet-string-length 50 --unwind 50 --java-assume-inputs-non-null
4-
^EXIT=10$
3+
--function Test.check --max-nondet-string-length 50 --unwind 50 --java-assume-inputs-non-null --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
4+
VERIFICATION SUCCESSFUL
5+
^EXIT=0$
56
^SIGNAL=0$
6-
assertion at file Test.java line 32 .* SUCCESS$
7-
assertion at file Test.java line 34 .* FAILURE$

‎jbmc/regression/strings-smoke-tests/java_format5/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
THOROUGH
1+
CORE
22
test
3-
--max-nondet-string-length 20
3+
--function test.main --max-nondet-string-length 20 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
^\[.*assertion.1\].* line 7.* SUCCESS$

‎jbmc/regression/strings-smoke-tests/java_long_to_string/test2.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
THOROUGH
1+
CORE
22
Test2
3-
--max-nondet-string-length 1000 --function Test2.main
3+
--max-nondet-string-length 1000 --function Test2.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
assertion.* line 7 .* SUCCESS$

‎jbmc/regression/strings-smoke-tests/java_long_to_string/test3.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
THOROUGH
1+
CORE
22
Test3
3-
--max-nondet-string-length 1000 --function Test3.main
3+
--max-nondet-string-length 1000 --function Test3.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
assertion.* line 7 .* SUCCESS$

‎jbmc/regression/strings-smoke-tests/java_long_to_string/test4.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
THOROUGH
1+
CORE
22
Test4
3-
--max-nondet-string-length 1000 --function Test4.main
3+
--max-nondet-string-length 1000 --function Test4.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
assertion.* line 7 .* SUCCESS$

‎jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary1.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
THOROUGH
1+
CORE
22
Test_binary1
3-
--max-nondet-string-length 1000 --function Test_binary1.main
3+
--max-nondet-string-length 1000 --function Test_binary1.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
assertion.* line 7 .* SUCCESS$

‎jbmc/regression/strings-smoke-tests/java_long_to_string_with_radix/test_binary2.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
1-
THOROUGH
1+
CORE
22
Test_binary2
3-
--max-nondet-string-length 1000 --function Test_binary2.main
3+
--max-nondet-string-length 1000 --function Test_binary2.main --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
44
^EXIT=10$
55
^SIGNAL=0$
66
assertion.* line 7 .* SUCCESS$

0 commit comments

Comments
 (0)