Skip to content

Commit ce66557

Browse files
committed
Add regression/libcprover-cpp to Makefile builds
Ensure that both CMake and Make run the same set of tests, and facilitate cleanup after running tests (for either build system).
1 parent 13537d2 commit ce66557

File tree

4 files changed

+55
-1
lines changed

4 files changed

+55
-1
lines changed

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -69,7 +69,7 @@ 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

regression/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -62,6 +62,7 @@ DIRS = cbmc-shadow-memory \
6262
cbmc-sequentialization \
6363
cpp-linter \
6464
catch-framework \
65+
libcprover-cpp \
6566
# Empty last line
6667

6768
ifeq ($(OS),Windows_NT)

regression/libcprover-cpp/Makefile

Lines changed: 41 additions & 0 deletions
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
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 ../../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

0 commit comments

Comments
 (0)