Skip to content

Commit 13537d2

Browse files
committed
Add regression/goto-bmc to Makefile builds
These tests should also be run when using Makefile-based builds, and Makefiles are the only way to perform cleanup.
1 parent f01545d commit 13537d2

File tree

5 files changed

+57
-2
lines changed

5 files changed

+57
-2
lines changed

regression/Makefile

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -30,6 +30,9 @@ DIRS = cbmc-shadow-memory \
3030
goto-diff \
3131
test-script \
3232
goto-analyzer-taint \
33+
goto-bmc/goto-bmc-symex-ready-goto \
34+
goto-bmc/goto-bmc-non-symex-ready-goto \
35+
goto-bmc \
3336
goto-gcc \
3437
goto-cl \
3538
goto-cc-cbmc \

regression/goto-bmc/Makefile

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
default: tests.log
2+
3+
test:
4+
@../test.pl -e -p -c ../../../src/goto-bmc/goto-bmc
5+
6+
tests.log: ../test.pl
7+
@../test.pl -e -p -c ../../../src/goto-bmc/goto-bmc
8+
9+
clean:
10+
find . -name '*.out' -execdir $(RM) '{}' \;
11+
find . -name '*.gb' -execdir $(RM) '{}' \;
12+
$(RM) tests.log
Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
default: tests.log
2+
3+
include ../../../src/config.inc
4+
include ../../../src/common
5+
6+
GOTO_BMC_EXE=../../../../src/goto-bmc/goto-bmc
7+
8+
ifeq ($(BUILD_ENV_),MSVC)
9+
GOTO_CC_EXE=../../../../src/goto-cc/goto-cl
10+
is_windows=true
11+
else
12+
GOTO_CC_EXE=../../../../src/goto-cc/goto-cc
13+
is_windows=false
14+
endif
15+
16+
test:
17+
@../../test.pl -e -p -c "../chain.sh $(GOTO_CC_EXE) $(GOTO_BMC_EXE) $(is_windows)"
18+
19+
tests.log: ../test.pl
20+
@../../test.pl -e -p -c "../chain.sh $(GOTO_CC_EXE) $(GOTO_BMC_EXE) $(is_windows)"
21+
22+
clean:
23+
find . -name '*.out' -execdir $(RM) '{}' \;
24+
find . -name '*.gb' -execdir $(RM) {} \;
25+
$(RM) tests.log
Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
default: tests.log
2+
3+
CBMC_EXE=../../../../src/cbmc/cbmc
4+
GOTO_BMC_EXE=../../../../src/goto-bmc/goto-bmc
5+
6+
test:
7+
@../../test.pl -e -p -c "../chain.sh $(CBMC_EXE) $(GOTO_BMC_EXE)"
8+
9+
tests.log: ../test.pl
10+
@../../test.pl -e -p -c "../chain.sh $(CBMC_EXE) $(GOTO_BMC_EXE)"
11+
12+
clean:
13+
find . -name '*.out' -execdir $(RM) '{}' \;
14+
find . -name '*.gb' -execdir $(RM) {} \;
15+
$(RM) tests.log

regression/goto-bmc/goto-bmc-symex-ready-goto/chain.sh

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -9,5 +9,5 @@ options=${*:3:$#-3}
99
name=${*:$#}
1010
base_name=${name%.c}
1111

12-
"${cbmc}" --export-symex-ready-goto "${base_name}.goto.symex_ready" "${name}"
13-
"${goto_bmc}" "${base_name}.goto.symex_ready" ${options}
12+
"${cbmc}" --export-symex-ready-goto "${base_name}.gb" "${name}"
13+
"${goto_bmc}" "${base_name}.gb" ${options}

0 commit comments

Comments
 (0)