Skip to content

Commit c1c0356

Browse files
tautschnigtautschnig
authored
Merge pull request #5557 from tautschnig/sequentialisation-regression-build-fix
Synchronise Makefile and CMake configuration of regression tests
2 parents 57c5505 + b3e591b commit c1c0356

File tree

12 files changed

+35
-24
lines changed

12 files changed

+35
-24
lines changed

‎regression/CMakeLists.txt

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -58,6 +58,10 @@ add_subdirectory(goto-cc-file-local)
5858
add_subdirectory(goto-cc-regression-gh-issue-5380)
5959
add_subdirectory(linking-goto-binaries)
6060
add_subdirectory(symtab2gb)
61+
add_subdirectory(solver-hardness)
62+
if(NOT WIN32)
63+
add_subdirectory(goto-ld)
64+
endif()
6165
add_subdirectory(validate-trace-xml-schema)
6266
add_subdirectory(cbmc-primitives)
6367
add_subdirectory(goto-interpreter)
@@ -67,8 +71,3 @@ if(WITH_MEMORY_ANALYZER)
6771
add_subdirectory(snapshot-harness)
6872
add_subdirectory(memory-analyzer)
6973
endif()
70-
71-
add_subdirectory(solver-hardness)
72-
if(NOT WIN32)
73-
add_subdirectory(goto-ld)
74-
endif()

‎regression/Makefile

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,14 +19,16 @@ DIRS = cbmc \
1919
test-script \
2020
goto-analyzer-taint \
2121
goto-gcc \
22-
goto-harness \
2322
goto-cl \
2423
goto-cc-cbmc \
24+
goto-cc-cbmc-shared-options \
2525
cbmc-cpp \
2626
goto-cc-goto-analyzer \
2727
statement-list \
2828
systemc \
2929
contracts \
30+
goto-harness \
31+
goto-harness-multi-file-project \
3032
goto-cc-file-local \
3133
goto-cc-regression-gh-issue-5380 \
3234
linking-goto-binaries \
@@ -36,6 +38,7 @@ DIRS = cbmc \
3638
validate-trace-xml-schema \
3739
cbmc-primitives \
3840
goto-interpreter \
41+
cbmc-sequentialization \
3942
# Empty last line
4043

4144
ifeq ($(OS),Windows_NT)

‎regression/acceleration/accelerate.sh

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ case $a in
2929
esac
3030
done
3131

32-
$goto_cc $cfile -o $ofile
33-
$goto_instrument --inline --remove-pointers $ofile $instrfile
32+
$goto_cc $cfile -o $ofile || exit 1
33+
$goto_instrument --inline --remove-pointers $ofile $instrfile || exit 1
3434
timeout 5 $goto_instrument --accelerate $instrfile $accfile
3535
timeout 5 $cbmc --unwind 5 --z3 $cbmcargs $accfile

‎regression/cbmc-sequentialization/Makefile

Lines changed: 3 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -4,19 +4,13 @@ include ../../src/config.inc
44
include ../../src/common
55

66
ifeq ($(BUILD_ENV_),MSVC)
7-
GCC_ONLY = -X gcc-only
7+
POSIX_ONLY = -X requires_posix_only_headers
88
else
9-
GCC_ONLY =
9+
POSIX_ONLY =
1010
endif
1111

1212
test:
13-
@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" -X smt-backend $(GCC_ONLY)
14-
15-
test-cprover-smt2:
16-
@../test.pl -e -p -c "../../../src/cbmc/cbmc --cprover-smt2" -X broken-smt-backend $(GCC_ONLY)
17-
18-
test-paths-lifo:
19-
@../test.pl -e -p -c "../../../src/cbmc/cbmc --paths lifo" -X thorough-paths -X smt-backend -X paths-lifo-expected-failure $(GCC_ONLY)
13+
@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" $(POSIX_ONLY)
2014

2115
tests.log: ../test.pl test
2216

‎regression/goto-cc-cbmc-shared-options/Makefile

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,16 +6,18 @@ include ../../src/common
66
ifeq ($(BUILD_ENV_),MSVC)
77
exe=../../../src/goto-cc/goto-cl
88
is_windows=true
9+
exclude_broken_windows_tests=-X winbug
910
else
1011
exe=../../../src/goto-cc/goto-cc
1112
is_windows=false
13+
exclude_broken_windows_tests=
1214
endif
1315

1416
test:
15-
@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/cbmc/cbmc $(is_windows)'
17+
@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/cbmc/cbmc $(is_windows)' $(exclude_broken_windows_tests)
1618

1719
tests.log:
18-
@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/cbmc/cbmc $(is_windows)'
20+
@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/cbmc/cbmc $(is_windows)' $(exclude_broken_windows_tests)
1921

2022
show:
2123
@for dir in *; do \

‎regression/goto-cc-cbmc-shared-options/chain.sh

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,7 @@
11
#!/usr/bin/env bash
22

3+
set -e
4+
35
goto_cc=$1
46
cbmc=$2
57
is_windows=$3

‎regression/goto-cc-cbmc/chain.sh

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,7 @@
11
#!/usr/bin/env bash
22

3+
set -e
4+
35
goto_cc=$1
46
cbmc=$2
57
is_windows=$3

‎regression/goto-cc-goto-analyzer/chain.sh

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,7 @@
11
#!/usr/bin/env bash
22

3+
set -e
4+
35
goto_cc=$1
46
goto_analyzer=$2
57
is_windows=$3

‎regression/goto-cc-multi-file/chain.sh

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,7 @@
11
#!/usr/bin/env bash
22

3+
set -e
4+
35
goto_cc=$1
46
cbmc=$2
57
is_windows=$3

‎regression/goto-instrument-typedef/chain.sh

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,7 @@
11
#!/bin/bash
22

3+
set -e
4+
35
GC=$1
46
GI=$2
57
is_windows=$3
@@ -9,7 +11,7 @@ name=${name%.c}
911

1012
args=${*:4:$#-4}
1113

12-
rm "${name}.gb"
14+
rm -f "${name}.gb"
1315
if [[ "${is_windows}" == "true" ]]; then
1416
"$GC" "${name}.c" --function fun
1517
mv "${name}.exe" "${name}.gb"

‎regression/k-induction/chain.sh

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,7 @@
11
#!/bin/bash
22

3+
set -e
4+
35
src=../../../src
46
goto_cc=$src/goto-cc/goto-cc
57
goto_instrument=$src/goto-instrument/goto-instrument
@@ -16,9 +18,7 @@ k=$1
1618
$goto_cc -o $name.o $name.c
1719

1820
$goto_instrument --k-induction $k --base-case $name.o $name.base.o
19-
$cbmc $name.base.o
20-
if [ $? == 0 ] ; then echo "## Base case passes" ; else echo "## Base case fails" ; fi
21+
if $cbmc $name.base.o ; then echo "## Base case passes" ; else echo "## Base case fails" ; fi
2122

2223
$goto_instrument --k-induction $k --step-case $name.o $name.step.o
23-
$cbmc $name.step.o
24-
if [ $? == 0 ] ; then echo "## Step case passes" ; else echo "## Step case fails" ; fi
24+
if $cbmc $name.step.o ; then echo "## Step case passes" ; else echo "## Step case fails" ; fi

‎regression/symtab2gb/chain.sh

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,7 @@
11
#!/bin/bash
2+
3+
set -e
4+
25
symtab2gb_exe=$1
36
cbmc_exe=$2
47

0 commit comments

Comments
 (0)