1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
|
# For the best possible utilisation of multiple cores when
# running tests in parallel, it is important that these directories are
# listed with decreasing runtimes (i.e. longest running at the top)
DIRS = cbmc \
cbmc-library \
cprover \
crangler \
goto-analyzer \
ansi-c \
goto-instrument \
cpp \
cbmc-concurrency \
cbmc-cover \
cbmc-incr-oneloop \
cbmc-incr-smt2 \
cbmc-incr \
cbmc-output-file \
cbmc-with-incr \
array-refinement-with-incr \
goto-instrument-chc \
goto-instrument-json \
goto-instrument-wmm-core \
goto-instrument-typedef \
goto-inspect \
smt2_solver \
smt2_strings \
strings \
invariants \
goto-diff \
test-script \
goto-analyzer-taint \
goto-bmc/goto-bmc-symex-ready-goto \
goto-bmc/goto-bmc-non-symex-ready-goto \
goto-bmc \
goto-gcc \
goto-cl \
goto-cc-cbmc \
cbmc-cpp \
goto-cc-goto-analyzer \
goto-analyzer-simplify \
statement-list \
systemc \
contracts \
contracts-dfcc \
goto-synthesizer \
acceleration \
k-induction \
goto-harness \
goto-harness-multi-file-project \
goto-cc-file-local \
goto-cc-multi-file \
goto-cc-regression-gh-issue-5380 \
linking-goto-binaries \
symtab2gb \
symtab2gb-cbmc \
solver-hardness \
goto-ld \
validate-trace-xml-schema \
cbmc-primitives \
goto-interpreter \
cbmc-sequentialization \
cpp-linter \
catch-framework \
libcprover-cpp \
book-examples \
# Empty last line
ifndef WITH_MEMORY_ANALYZER
ifeq ($(OS),Windows_NT)
WITH_MEMORY_ANALYZER = 0
else
detected_OS := $(shell sh -c 'uname 2>/dev/null || echo Unknown')
detected_ARCH := $(shell sh -c 'uname -m 2>/dev/null || echo Unknown')
ifeq ($(filter-out Linux_x86_64 Linux_i386,$(detected_OS)_$(detected_ARCH)),)
WITH_MEMORY_ANALYZER = 1
else
WITH_MEMORY_ANALYZER = 0
endif
endif
endif
ifeq ($(WITH_MEMORY_ANALYZER),1)
DIRS += snapshot-harness \
memory-analyzer \
extract_type_header
endif
# Run all test directories in sequence
.PHONY: test
test:
@for dir in $(DIRS); do \
$(MAKE) "$$dir" || exit 1; \
done;
# Pattern to execute a single test suite directory
.PHONY: $(DIRS)
$(DIRS):
@echo "Running $@..." ;
$(MAKE) -C "$@" test || exit 1;
# Run all test directories using GNU Parallel
.PHONY: test-parallel
.NOTPARALLEL: test-parallel
test-parallel:
@echo "Building with $(JOBS) jobs"
parallel \
--halt soon,fail=1 \
--tag \
--tagstring '{#}:' \
--linebuffer \
--jobs $(JOBS) \
$(MAKE) "{}" \
::: $(DIRS)
.PHONY: clean
clean:
@for dir in $(DIRS); do \
$(MAKE) -C "$$dir" clean; \
done;
$(RM) tests.log
|
