Skip to content

Commit 1e8a703

Browse files
tautschnigtautschnig
authored
Merge pull request #7798 from tautschnig/cleanup/cleaning
Add missing cleanup
2 parents bcf6f4f + da99314 commit 1e8a703

File tree

22 files changed

+247
-11
lines changed

22 files changed

+247
-11
lines changed

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

+26-1
Original file line numberDiff line numberDiff line change
@@ -69,10 +69,24 @@ jobs:
6969
make TAGS="[!shouldfail]" -C jbmc/unit test IPASIR=$PWD/riss.git/riss
7070
- name: Run regression tests
7171
run: |
72-
make -C regression test-parallel JOBS=2
72+
make -C regression test-parallel JOBS=2 LIBS="$PWD/riss.git/release/lib/libriss-coprocessor.a -lpthread" IPASIR=$PWD/riss.git/riss
7373
make -C regression/cbmc test-paths-lifo
7474
env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2
7575
make -C jbmc/regression test-parallel JOBS=2
76+
- name: Check cleanup
77+
run: |
78+
make -C src clean IPASIR=$PWD/riss.git/riss
79+
make -C jbmc/src clean IPASIR=$PWD/riss.git/riss
80+
rm -r riss.git
81+
rm src/goto-cc/goto-ld
82+
make -C unit clean
83+
make -C regression clean
84+
make -C jbmc/unit clean
85+
make -C jbmc/regression clean
86+
if [[ $(git status --ignored --porcelain | grep -v .ccache/) ]] ; then
87+
git status --ignored
88+
exit 1
89+
fi
7690
7791
# This job takes approximately 25 to 34 minutes
7892
check-ubuntu-20_04-make-clang:
@@ -241,6 +255,17 @@ jobs:
241255
ls *.deb
242256
- name: Run tests
243257
run: cd build; ctest . -V -L CORE -j2
258+
- name: Check cleanup
259+
run: |
260+
rm -r build
261+
rm scripts/bash-autocomplete/cbmc.sh
262+
make -C unit clean
263+
make -C regression clean
264+
make -C jbmc/regression clean
265+
if [[ $(git status --ignored --porcelain | grep -v .ccache/) ]] ; then
266+
git status --ignored
267+
exit 1
268+
fi
244269
245270
# This job takes approximately 34 to 38 minutes
246271
check-ubuntu-22_04-make-clang:

‎regression/Makefile

+6-4
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 \
@@ -59,6 +62,7 @@ DIRS = cbmc-shadow-memory \
5962
cbmc-sequentialization \
6063
cpp-linter \
6164
catch-framework \
65+
libcprover-cpp \
6266
# Empty last line
6367

6468
ifeq ($(OS),Windows_NT)
@@ -110,9 +114,7 @@ test-parallel:
110114

111115
.PHONY: clean
112116
clean:
113-
@for dir in *; do \
114-
if [ -d "$$dir" ]; then \
115-
$(MAKE) -C "$$dir" clean; \
116-
fi; \
117+
@for dir in $(DIRS); do \
118+
$(MAKE) -C "$$dir" clean; \
117119
done;
118120
$(RM) tests.log

‎regression/ansi-c/Makefile

+1-1
Original file line numberDiff line numberDiff line change
@@ -64,4 +64,4 @@ build_goto_binaries:
6464
clean:
6565
find . -name '*.out' -execdir $(RM) '{}' \;
6666
find . -name '*.gb' -execdir $(RM) '{}' \;
67-
$(RM) tests.log tests-c++-front-end.log
67+
$(RM) tests*.log

‎regression/catch-framework/Makefile

+1
Original file line numberDiff line numberDiff line change
@@ -6,4 +6,5 @@ test:
66
tests.log: ../test.pl test
77

88
clean:
9+
find . -name '*.out' -execdir $(RM) '{}' \;
910
$(RM) tests*.log

‎regression/cbmc-primitives/Makefile

+1-1
Original file line numberDiff line numberDiff line change
@@ -11,4 +11,4 @@ tests.log: ../test.pl
1111

1212
clean:
1313
find . -name '*.out' -execdir $(RM) '{}' \;
14-
$(RM) tests.log
14+
$(RM) tests*.log

‎regression/cbmc/Makefile

+1
Original file line numberDiff line numberDiff line change
@@ -39,4 +39,5 @@ tests.log: ../test.pl test
3939
clean:
4040
find . -name '*.out' -execdir $(RM) '{}' \;
4141
find . -name '*.smt2' -execdir $(RM) '{}' \;
42+
$(RM) export-symex-ready-goto/exported.symex.ready.goto
4243
$(RM) tests*.log

‎regression/contracts-dfcc/Makefile

+1-1
Original file line numberDiff line numberDiff line change
@@ -34,10 +34,10 @@ tests.log: ../test.pl test
3434

3535
clean:
3636
@for dir in *; do \
37-
$(RM) tests.log; \
3837
if [ -d "$$dir" ]; then \
3938
cd "$$dir"; \
4039
$(RM) *.out *.gb *.smt2; \
4140
cd ..; \
4241
fi \
4342
done
43+
$(RM) tests*.log

‎regression/cprover/Makefile

+1
Original file line numberDiff line numberDiff line change
@@ -10,4 +10,5 @@ test-no-p:
1010
@../test.pl -e -c '../../../src/cprover/cprover'
1111

1212
clean:
13+
find . -name '*.out' -execdir $(RM) '{}' \;
1314
$(RM) tests.log

‎regression/goto-bmc/Makefile

+12
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

‎regression/goto-bmc/goto-bmc-non-symex-ready-goto/Makefile

+25
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

‎regression/goto-bmc/goto-bmc-symex-ready-goto/Makefile

+15
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

+2-2
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}

‎regression/goto-harness/Makefile

+1
Original file line numberDiff line numberDiff line change
@@ -23,4 +23,5 @@ tests.log: ../test.pl
2323
clean:
2424
find . -name '*.out' -execdir $(RM) '{}' \;
2525
find . -name '*.gb' -execdir $(RM) {} \;
26+
find . -name '*-harness.c' -execdir $(RM) {} \;
2627
$(RM) tests.log

‎regression/goto-instrument/Makefile

+1
Original file line numberDiff line numberDiff line change
@@ -26,3 +26,4 @@ clean:
2626
cd ..; \
2727
fi \
2828
done
29+
$(RM) ../cbmc/Recursion6/*.gb

‎regression/libcprover-cpp/Makefile

+41
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,41 @@
1+
default: tests.log
2+
3+
SRC = call_bmc.cpp $(wildcard ../../src/libcprover-cpp/*.cpp)
4+
5+
OBJ += ../../src/libcprover-cpp/libcprover-cpp$(LIBEXT)
6+
7+
INCLUDES = -I ../../src/ -I ../../src/goto-programs/
8+
9+
CLEANFILES = api-binary-driver$(EXEEXT)
10+
11+
include ../../src/config.inc
12+
include ../../src/common
13+
14+
api-binary-driver$(EXEEXT): $(OBJ)
15+
$(LINKBIN)
16+
17+
DIRS = \
18+
model_loading
19+
20+
test:
21+
@for dir in $(DIRS); do \
22+
$(MAKE) -C "$$dir" test || exit 1; \
23+
done;
24+
25+
tests.log:
26+
@for dir in $(DIRS); do \
27+
$(MAKE) -C "$$dir" tests.log || exit 1; \
28+
done;
29+
30+
test tests.log: api-binary-driver$(EXEEXT)
31+
32+
clean: regression_clean
33+
34+
.PHONY: regression_clean
35+
regression_clean:
36+
@for dir in *; do \
37+
if [ -d "$$dir" ]; then \
38+
$(MAKE) -C "$$dir" clean; \
39+
fi; \
40+
done;
41+
$(RM) tests.log

‎regression/libcprover-cpp/model_loading/Makefile

+12
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 ../../api-binary-driver
5+
6+
tests.log:
7+
@../../test.pl -e -p -c ../../api-binary-driver
8+
9+
clean:
10+
find . -name '*.out' -execdir $(RM) '{}' \;
11+
find . -name '*.gb' -execdir $(RM) '{}' \;
12+
$(RM) tests.log

‎regression/solver-hardness/Makefile

+1
Original file line numberDiff line numberDiff line change
@@ -16,4 +16,5 @@ tests.log: ../test.pl test
1616

1717
clean:
1818
find . -name '*.out' -execdir $(RM) '{}' \;
19+
find . -name '*.json' -execdir $(RM) '{}' \;
1920
$(RM) tests.log

‎regression/validate-trace-xml-schema/check.py

+1
Original file line numberDiff line numberDiff line change
@@ -41,6 +41,7 @@
4141
# these test for invalid command line handling
4242
['bad_option', 'test_multiple.desc'],
4343
['bad_option', 'test.desc'],
44+
['export-symex-ready-goto', 'test-bad-usage.desc'],
4445
['unknown-argument-suggestion', 'test.desc'],
4546
['sat-solver-error', 'test.desc'],
4647
# this one produces XML intermingled with main XML output when used with --xml-ui

‎src/Makefile

+7
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@ DIRS = analyses \
77
cprover \
88
crangler \
99
goto-analyzer \
10+
goto-bmc \
1011
goto-cc \
1112
goto-checker \
1213
goto-diff \
@@ -20,6 +21,7 @@ DIRS = analyses \
2021
json \
2122
json-symtab-language \
2223
langapi \
24+
libcprover-cpp \
2325
linking \
2426
memory-analyzer \
2527
pointer-analysis \
@@ -34,6 +36,7 @@ all: cbmc.dir \
3436
cprover.dir \
3537
crangler.dir \
3638
goto-analyzer.dir \
39+
goto-bmc.dir \
3740
goto-cc.dir \
3841
goto-diff.dir \
3942
goto-instrument.dir \
@@ -114,6 +117,10 @@ goto-synthesizer.dir: languages util.dir goto-programs.dir langapi.dir \
114117
json.dir goto-checker.dir \
115118
goto-instrument.dir
116119

120+
goto-bmc.dir: libcprover-cpp.dir
121+
122+
libcprover-cpp.dir: cbmc.dir
123+
117124
# building for a particular directory
118125

119126
$(patsubst %, %.dir, $(DIRS)):

‎src/goto-bmc/Makefile

+29
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
SRC = \
2+
goto_bmc_main.cpp \
3+
goto_bmc_parse_options.cpp \
4+
# Empty last line
5+
6+
OBJ += \
7+
../libcprover-cpp/libcprover-cpp$(LIBEXT) \
8+
# Empty last line
9+
10+
INCLUDES= -I .. -I ../libcprover-cpp
11+
12+
LIBS =
13+
14+
CLEANFILES = goto-bmc$(EXEEXT)
15+
16+
include ../config.inc
17+
include ../common
18+
19+
all: goto-bmc$(EXEEXT)
20+
21+
###############################################################################
22+
23+
goto-bmc$(EXEEXT): $(OBJ)
24+
$(LINKBIN)
25+
26+
.PHONY: goto-bmc-mac-signed
27+
28+
goto-bmc-mac-signed: goto-bmc$(EXEEXT)
29+
codesign -v -s $(OSX_IDENTITY) goto-bmc$(EXEEXT)

‎src/libcprover-cpp/Makefile

+61
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,61 @@
1+
SRC = \
2+
api.cpp \
3+
api_options.cpp \
4+
verification_result.cpp \
5+
# Empty last line
6+
7+
OBJ += \
8+
../analyses/analyses$(LIBEXT) \
9+
../ansi-c/ansi-c$(LIBEXT) \
10+
../assembler/assembler$(LIBEXT) \
11+
../big-int/big-int$(LIBEXT) \
12+
../goto-checker/goto-checker$(LIBEXT) \
13+
../goto-instrument/cover$(OBJEXT) \
14+
../goto-instrument/cover_basic_blocks$(OBJEXT) \
15+
../goto-instrument/cover_filter$(OBJEXT) \
16+
../goto-instrument/cover_instrument_assume$(OBJEXT) \
17+
../goto-instrument/cover_instrument_branch$(OBJEXT) \
18+
../goto-instrument/cover_instrument_condition$(OBJEXT) \
19+
../goto-instrument/cover_instrument_decision$(OBJEXT) \
20+
../goto-instrument/cover_instrument_location$(OBJEXT) \
21+
../goto-instrument/cover_instrument_mcdc$(OBJEXT) \
22+
../goto-instrument/cover_instrument_other$(OBJEXT) \
23+
../goto-instrument/cover_util$(OBJEXT) \
24+
../goto-instrument/full_slicer$(OBJEXT) \
25+
../goto-instrument/nondet_static$(OBJEXT) \
26+
../goto-instrument/reachability_slicer$(OBJEXT) \
27+
../goto-instrument/source_lines$(OBJEXT) \
28+
../goto-instrument/unwindset$(OBJEXT) \
29+
../goto-programs/goto-programs$(LIBEXT) \
30+
../goto-symex/goto-symex$(LIBEXT) \
31+
../jsil/jsil$(LIBEXT) \
32+
../json-symtab-language/json-symtab-language$(LIBEXT) \
33+
../json/json$(LIBEXT) \
34+
../langapi/langapi$(LIBEXT) \
35+
../linking/linking$(LIBEXT) \
36+
../pointer-analysis/add_failed_symbols$(OBJEXT) \
37+
../pointer-analysis/goto_program_dereference$(OBJEXT) \
38+
../pointer-analysis/value_set$(OBJEXT) \
39+
../pointer-analysis/value_set_analysis_fi$(OBJEXT) \
40+
../pointer-analysis/value_set_dereference$(OBJEXT) \
41+
../pointer-analysis/value_set_domain_fi$(OBJEXT) \
42+
../pointer-analysis/value_set_fi$(OBJEXT) \
43+
../solvers/solvers$(LIBEXT) \
44+
../statement-list/statement-list$(LIBEXT) \
45+
../util/util$(LIBEXT) \
46+
../xmllang/xmllang$(LIBEXT) \
47+
# Empty last line
48+
49+
INCLUDES = -I ..
50+
51+
include ../config.inc
52+
include ../common
53+
54+
CLEANFILES = libcprover-cpp$(LIBEXT)
55+
56+
all: libcprover-cpp$(LIBEXT)
57+
58+
###############################################################################
59+
60+
libcprover-cpp$(LIBEXT): $(OBJ)
61+
$(LINKLIB)

‎unit/Makefile

+1-1
Original file line numberDiff line numberDiff line change
@@ -303,7 +303,7 @@ memory-analyzer/test.inc: memory-analyzer/test.c
303303
memory-analyzer/gdb_api$(OBJEXT): memory-analyzer/input.inc memory-analyzer/test.inc
304304

305305
CLEANFILES = $(CATCH_TEST) testing-utils/testing-utils$(LIBEXT) \
306-
memory-analyzer/input.inc memory-analyzer/test.inc
306+
memory-analyzer/input.inc memory-analyzer/test.inc gdb.txt
307307

308308
# only add a dependency for libraries to avoid triggering implicit rules, which
309309
# would cause unnecessary rebuilds

0 commit comments

Comments
 (0)