Skip to content

Commit f55bd96

Browse files
peterschrammelpeterschrammel
authored
Merge pull request diffblue#2231 from smowton/smowton/fix/jbmc-tests
Restore testing of jbmc
2 parents af02973 + 42a78af commit f55bd96

File tree

13 files changed

+46
-58
lines changed

13 files changed

+46
-58
lines changed

‎.gitignore

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -57,6 +57,7 @@ regression/**/tests.log
5757
regression/**/*.gb
5858
regression/**/*.smt2
5959
jbmc/regression/**/tests.log
60+
jbmc/regression/**/tests-symex-driven-loading.log
6061

6162
# regression/coverage file
6263
/regression/coverage_**

‎CMakeLists.txt

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -34,14 +34,15 @@ set(sat_impl "minisat2" CACHE STRING
3434
"This setting controls the SAT library which is used. Valid values are 'minisat2' and 'glucose'"
3535
)
3636

37-
add_subdirectory(src)
38-
add_subdirectory(jbmc)
39-
4037
if(${enable_cbmc_tests})
4138
enable_testing()
4239
endif()
43-
add_subdirectory(unit)
40+
41+
add_subdirectory(src)
4442
add_subdirectory(regression)
43+
add_subdirectory(unit)
44+
45+
add_subdirectory(jbmc)
4546

4647
set_target_properties(
4748
analyses

‎jbmc/regression/CMakeLists.txt

Lines changed: 1 addition & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -1,24 +1,4 @@
1-
set(test_pl_path "${CMAKE_CURRENT_SOURCE_DIR}/test.pl")
2-
3-
macro(add_test_pl_profile name cmdline flag profile)
4-
add_test(
5-
NAME "${name}-${profile}"
6-
COMMAND ${test_pl_path} -p -c ${cmdline} ${flag} ${ARGN}
7-
WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}"
8-
)
9-
set_tests_properties("${name}-${profile}" PROPERTIES
10-
LABELS "${profile};CBMC"
11-
)
12-
endmacro(add_test_pl_profile)
13-
14-
macro(add_test_pl_tests cmdline)
15-
get_filename_component(TEST_DIR_NAME ${CMAKE_CURRENT_SOURCE_DIR} NAME)
16-
message(STATUS "Adding tests in directory: ${TEST_DIR_NAME}")
17-
add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -C CORE ${ARGN})
18-
add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -T THOROUGH ${ARGN})
19-
add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -F FUTURE ${ARGN})
20-
add_test_pl_profile("${TEST_DIR_NAME}" "${cmdline}" -K KNOWNBUG ${ARGN})
21-
endmacro(add_test_pl_tests)
1+
set(test_pl_path "${CMAKE_SOURCE_DIR}/regression/test.pl")
222

233
# For the best possible utilisation of multiple cores when
244
# running tests in parallel, it is important that these directories are

‎jbmc/regression/janalyzer-taint/CMakeLists.txt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
11
add_test_pl_tests(
2-
"$<TARGET_FILE:goto-analyzer>"
2+
"$<TARGET_FILE:janalyzer>"
33
)

‎jbmc/regression/jbmc-cover/CMakeLists.txt

Lines changed: 0 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,3 @@
11
add_test_pl_tests(
22
"$<TARGET_FILE:jbmc>"
33
)
4-
5-
add_test_pl_profile(
6-
"cbmc-java-symex-driven-lazy-loading"
7-
"$<TARGET_FILE:jbmc> --symex-driven-lazy-loading"
8-
"-C;-X;symex-driven-lazy-loading-expected-failure"
9-
"CORE"
10-
)

‎jbmc/regression/jbmc-strings/CMakeLists.txt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,6 @@ add_test_pl_tests(
55
add_test_pl_profile(
66
"jbmc-strings-symex-driven-lazy-loading"
77
"$<TARGET_FILE:jbmc> --symex-driven-lazy-loading"
8-
"-C;-X;symex-driven-lazy-loading-expected-failure"
8+
"-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading"
99
"CORE"
1010
)

‎jbmc/regression/jbmc-strings/Makefile

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

55
test:
66
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
7-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure
7+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
88

99
testfuture:
1010
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc -CF
11-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF
11+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF -s symex-driven-loading
1212

1313
testall:
1414
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc -CFTK
15-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK
15+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK -s symex-driven-loading
1616

1717
tests.log: ../$(CPROVER_DIR)/regression/test.pl
1818
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
19-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure
19+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
2020

2121
show:
2222
@for dir in *; do \
@@ -29,4 +29,3 @@ clean:
2929
find -name '*.out' -execdir $(RM) '{}' \;
3030
find -name '*.gb' -execdir $(RM) '{}' \;
3131
$(RM) tests.log
32-

‎jbmc/regression/jbmc/CMakeLists.txt

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@ add_test_pl_tests(
33
)
44

55
add_test_pl_profile(
6-
"cbmc-java-symex-driven-lazy-loading"
6+
"jbmc-symex-driven-lazy-loading"
77
"$<TARGET_FILE:jbmc> --symex-driven-lazy-loading"
8-
"-C;-X;symex-driven-lazy-loading-expected-failure"
8+
"-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading"
99
"CORE"
1010
)

‎jbmc/regression/jbmc/Makefile

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,11 +4,11 @@ include ../../src/config.inc
44

55
test:
66
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
7-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure
7+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
88

99
tests.log: ../$(CPROVER_DIR)/regression/test.pl
1010
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
11-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure
11+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
1212

1313
show:
1414
@for dir in *; do \

‎jbmc/regression/jdiff/CMakeLists.txt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
11
add_test_pl_tests(
2-
"$<TARGET_FILE:goto-diff>"
2+
"$<TARGET_FILE:jdiff>"
33
)

‎jbmc/regression/strings-smoke-tests/CMakeLists.txt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,6 @@ add_test_pl_tests(
55
add_test_pl_profile(
66
"strings-smoke-tests-symex-driven-lazy-loading"
77
"$<TARGET_FILE:jbmc> --symex-driven-lazy-loading"
8-
"-C;-X;symex-driven-lazy-loading-expected-failure"
8+
"-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading"
99
"CORE"
1010
)

‎jbmc/regression/strings-smoke-tests/Makefile

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

55
test:
66
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
7-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure
7+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
88

99
testfuture:
1010
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc -CF
11-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF
11+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF -s symex-driven-loading
1212

1313
testall:
1414
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc -CFTK
15-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK
15+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK -s symex-driven-loading
1616

1717
tests.log: ../$(CPROVER_DIR)/regression/test.pl
1818
@../$(CPROVER_DIR)/regression/test.pl -p -c ../../../src/jbmc/jbmc
19-
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure
19+
@../$(CPROVER_DIR)/regression/test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading
2020

2121
show:
2222
@for dir in *; do \
@@ -29,4 +29,3 @@ clean:
2929
find -name '*.out' -execdir $(RM) '{}' \;
3030
find -name '*.gb' -execdir $(RM) '{}' \;
3131
$(RM) tests.log
32-

‎regression/test.pl

Lines changed: 23 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -66,8 +66,8 @@ ($)
6666
return @data;
6767
}
6868

69-
sub test($$$$$$$$$) {
70-
my ($name, $test, $t_level, $cmd, $ign, $dry_run, $defines, $include_tags, $exclude_tags) = @_;
69+
sub test($$$$$$$$$$) {
70+
my ($name, $test, $t_level, $cmd, $ign, $dry_run, $defines, $include_tags, $exclude_tags, $output_suffix) = @_;
7171
my ($level_and_tags, $input, $options, $grep_options, @results) = load("$test");
7272
my @keys = keys %{$defines};
7373
foreach my $key (@keys) {
@@ -115,7 +115,12 @@ ($$$$$$$$$)
115115

116116
my $descriptor = basename($test);
117117
my $output = $descriptor;
118-
$output =~ s/\.[^.]*$/.out/;
118+
$output =~ s/\.[^.]*$//;
119+
if($output_suffix) {
120+
$output .= "-";
121+
$output .= $output_suffix;
122+
}
123+
$output .= ".out";
119124

120125
if($output eq $input) {
121126
print("Error in test file -- $test\n");
@@ -269,7 +274,10 @@ ($$$$)
269274
test descriptors
270275
-I <tag> run only tests that have the given secondary tag. Can be repeated.
271276
-X <tag> exclude tests that have the given secondary tag. Can be repeated.
272-
277+
-s <suffix> append <suffix> to all output and log files. Enables concurrent
278+
testing of the same desc file with different commands or options,
279+
as runs with different suffixes will operate independently and keep
280+
independent logs.
273281
274282
test.pl expects a test.desc file in each subdirectory. The file test.desc
275283
follows the format specified below. Any line starting with // will be ignored.
@@ -304,9 +312,9 @@ ($$$$)
304312
use Getopt::Long qw(:config pass_through bundling);
305313
$main::VERSION = 0.1;
306314
$Getopt::Std::STANDARD_HELP_VERSION = 1;
307-
our ($opt_c, $opt_i, $opt_j, $opt_n, $opt_p, $opt_h, $opt_C, $opt_T, $opt_F, $opt_K, %defines, @include_tags, @exclude_tags); # the variables for getopt
315+
our ($opt_c, $opt_i, $opt_j, $opt_n, $opt_p, $opt_h, $opt_C, $opt_T, $opt_F, $opt_K, $opt_s, %defines, @include_tags, @exclude_tags); # the variables for getopt
308316
GetOptions("D=s" => \%defines, "X=s" => \@exclude_tags, "I=s" => \@include_tags);
309-
getopts('c:i:j:nphCTFK') or &main::HELP_MESSAGE(\*STDOUT, "", $main::VERSION, "");
317+
getopts('c:i:j:nphCTFKs:') or &main::HELP_MESSAGE(\*STDOUT, "", $main::VERSION, "");
310318
$opt_c or &main::HELP_MESSAGE(\*STDOUT, "", $main::VERSION, "");
311319
$opt_j = $opt_j || $ENV{'TESTPL_JOBS'} || 0;
312320
if($opt_j && $opt_j != 1 && !$has_thread_pool) {
@@ -321,9 +329,16 @@ ($$$$)
321329
$t_level += 8 if($opt_K);
322330
$t_level += 1 if($opt_C || 0 == $t_level);
323331
my $dry_run = $opt_n;
332+
my $log_suffix = $opt_s;
324333

334+
my $logfile_name = "tests";
335+
if($log_suffix) {
336+
$logfile_name .= "-";
337+
$logfile_name .= $log_suffix;
338+
}
339+
$logfile_name .= ".log";
325340

326-
open LOG,">tests.log";
341+
open LOG, (">" . $logfile_name);
327342

328343
print "Loading\n";
329344
my @tests = @ARGV != 0 ? @ARGV : dirs();
@@ -349,7 +364,7 @@ ($)
349364
defined($pool) or print " Running $files[$_]";
350365
my $start_time = time();
351366
$failed_skipped = test(
352-
$test, $files[$_], $t_level, $opt_c, $opt_i, $dry_run, \%defines, \@include_tags, \@exclude_tags);
367+
$test, $files[$_], $t_level, $opt_c, $opt_i, $dry_run, \%defines, \@include_tags, \@exclude_tags, $log_suffix);
353368
my $runtime = time() - $start_time;
354369

355370
lock($skips);

0 commit comments

Comments
 (0)