diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt index e3bf553e7c5..7dec29c1ffa 100644 --- a/regression/CMakeLists.txt +++ b/regression/CMakeLists.txt @@ -6,7 +6,7 @@ set(test_pl_path "${CMAKE_CURRENT_SOURCE_DIR}/test.pl") macro(add_test_pl_profile name cmdline flag profile) add_test( NAME "${name}-${profile}" - COMMAND ${test_pl_path} -c ${cmdline} ${flag} + COMMAND ${test_pl_path} -p -c ${cmdline} ${flag} WORKING_DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}" ) set_tests_properties("${name}-${profile}" PROPERTIES @@ -34,6 +34,9 @@ add_subdirectory(goto-cc-goto-analyzer) add_subdirectory(goto-diff) add_subdirectory(goto-instrument) add_subdirectory(goto-instrument-typedef) +if(NOT WIN32) + add_subdirectory(goto-gcc) +endif() add_subdirectory(invariants) add_subdirectory(jbmc-strings) add_subdirectory(strings) diff --git a/regression/ansi-c/Makefile b/regression/ansi-c/Makefile index c770b3b3ed7..3146b15f028 100644 --- a/regression/ansi-c/Makefile +++ b/regression/ansi-c/Makefile @@ -10,16 +10,10 @@ else endif test: - @if ! ../test.pl -c $(exe) ; then \ - ../failed-tests-printer.pl ; \ - exit 1 ; \ - fi + @../test.pl -p -c $(exe) tests.log: ../test.pl - @if ! ../test.pl -c $(exe) ; then \ - ../failed-tests-printer.pl ; \ - exit 1 ; \ - fi + @../test.pl -p -c $(exe) show: @for dir in *; do \ diff --git a/regression/cbmc-cover/Makefile b/regression/cbmc-cover/Makefile index 9a14abc905f..486a8c750f7 100644 --- a/regression/cbmc-cover/Makefile +++ b/regression/cbmc-cover/Makefile @@ -1,16 +1,10 @@ default: tests.log test: - @if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \ - ../failed-tests-printer.pl ; \ - exit 1 ; \ - fi + @../test.pl -p -c ../../../src/cbmc/cbmc tests.log: ../test.pl - @if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \ - ../failed-tests-printer.pl ; \ - exit 1 ; \ - fi + @../test.pl -p -c ../../../src/cbmc/cbmc show: @for dir in *; do \ diff --git a/regression/cbmc-java-inheritance/Makefile b/regression/cbmc-java-inheritance/Makefile index 2aa697dd691..e94b327bb43 100644 --- a/regression/cbmc-java-inheritance/Makefile +++ b/regression/cbmc-java-inheritance/Makefile @@ -1,16 +1,10 @@ default: tests.log test: - @if ! ../test.pl -c ../../../src/jbmc/jbmc ; then \ - ../failed-tests-printer.pl ; \ - exit 1 ; \ - fi + @../test.pl -p -c ../../../src/jbmc/jbmc tests.log: ../test.pl - @if ! ../test.pl -c ../../../src/jbmc/jbmc ; then \ - ../failed-tests-printer.pl ; \ - exit 1 ; \ - fi + @../test.pl -p -c ../../../src/jbmc/jbmc show: @for dir in *; do \ diff --git a/regression/cbmc-java/Makefile b/regression/cbmc-java/Makefile index 2aa697dd691..e94b327bb43 100644 --- a/regression/cbmc-java/Makefile +++ b/regression/cbmc-java/Makefile @@ -1,16 +1,10 @@ default: tests.log test: - @if ! ../test.pl -c ../../../src/jbmc/jbmc ; then \ - ../failed-tests-printer.pl ; \ - exit 1 ; \ - fi + @../test.pl -p -c ../../../src/jbmc/jbmc tests.log: ../test.pl - @if ! ../test.pl -c ../../../src/jbmc/jbmc ; then \ - ../failed-tests-printer.pl ; \ - exit 1 ; \ - fi + @../test.pl -p -c ../../../src/jbmc/jbmc show: @for dir in *; do \ diff --git a/regression/cbmc-java/classpath2/test.desc b/regression/cbmc-java/classpath2/test.desc index ba3ea35b785..3f8043663f0 100644 --- a/regression/cbmc-java/classpath2/test.desc +++ b/regression/cbmc-java/classpath2/test.desc @@ -1,6 +1,6 @@ CORE jarfile3.class ---function jarfile3.f --java-cp-include-files "jarfile3\.class" +--function jarfile3.f --java-cp-include-files 'jarfile3\.class' ^EXIT=10$ ^SIGNAL=0$ .*SUCCESS$ diff --git a/regression/cbmc-java/function1/test.desc b/regression/cbmc-java/function1/test.desc index 3800f47f81a..2b01e276991 100644 --- a/regression/cbmc-java/function1/test.desc +++ b/regression/cbmc-java/function1/test.desc @@ -1,6 +1,6 @@ CORE Main.class ---function "Other.fail:()V" +--function 'Other.fail:()V' ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc-java/function2/test.desc b/regression/cbmc-java/function2/test.desc index 423018ec7c8..fd61e253b75 100644 --- a/regression/cbmc-java/function2/test.desc +++ b/regression/cbmc-java/function2/test.desc @@ -1,6 +1,6 @@ CORE Main.class ---function "D.fail:()V" +--function 'D.fail:()V' ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc-java/function3/test.desc b/regression/cbmc-java/function3/test.desc index c40b8ddc743..c1a23e0431e 100644 --- a/regression/cbmc-java/function3/test.desc +++ b/regression/cbmc-java/function3/test.desc @@ -1,6 +1,6 @@ KNOWNBUG Main.class ---function "A.dummy:()V" +--function 'A.dummy:()V' ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc-java/function4/test.desc b/regression/cbmc-java/function4/test.desc index d7aabbbb7e6..51d7c89999b 100644 --- a/regression/cbmc-java/function4/test.desc +++ b/regression/cbmc-java/function4/test.desc @@ -1,6 +1,6 @@ KNOWNBUG Main.class ---function "Other.fail" +--function 'Other.fail' ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc-java/jar-file4/test.desc b/regression/cbmc-java/jar-file4/test.desc index 5c34bdcd5a8..a3e8b295262 100644 --- a/regression/cbmc-java/jar-file4/test.desc +++ b/regression/cbmc-java/jar-file4/test.desc @@ -1,6 +1,6 @@ CORE C.jar ---function jarfile3.f --java-cp-include-files "@jar.json" +--function jarfile3.f --java-cp-include-files '@jar.json' ^EXIT=10$ ^SIGNAL=0$ .*SUCCESS$ diff --git a/regression/cbmc-java/lazyloading11/test.desc b/regression/cbmc-java/lazyloading11/test.desc index c74260ce902..1114831afb3 100644 --- a/regression/cbmc-java/lazyloading11/test.desc +++ b/regression/cbmc-java/lazyloading11/test.desc @@ -1,6 +1,6 @@ CORE test.class ---lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point "test.sety:(I)V" --lazy-methods-extra-entry-point "test.sety:(F)V" +--lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point 'test.sety:(I)V' --lazy-methods-extra-entry-point 'test.sety:(F)V' ^EXIT=0$ ^SIGNAL=0$ VERIFICATION SUCCESSFUL diff --git a/regression/cbmc-java/lazyloading7/test.desc b/regression/cbmc-java/lazyloading7/test.desc index 2d26cc1dfdb..3b2e305f66c 100644 --- a/regression/cbmc-java/lazyloading7/test.desc +++ b/regression/cbmc-java/lazyloading7/test.desc @@ -1,6 +1,6 @@ CORE test.class ---lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point "test.sety:(I)V" +--lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point 'test.sety:(I)V' ^EXIT=0$ ^SIGNAL=0$ VERIFICATION SUCCESSFUL diff --git a/regression/cbmc-java/lazyloading8/test.desc b/regression/cbmc-java/lazyloading8/test.desc index afad44d2c8f..777f1673de9 100644 --- a/regression/cbmc-java/lazyloading8/test.desc +++ b/regression/cbmc-java/lazyloading8/test.desc @@ -1,6 +1,6 @@ CORE test.class ---lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point "test.sety:(F)V" +--lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point 'test.sety:(F)V' ^EXIT=0$ ^SIGNAL=0$ VERIFICATION SUCCESSFUL diff --git a/regression/cbmc-java/lazyloading9/test.desc b/regression/cbmc-java/lazyloading9/test.desc index aa4ccefe783..ddd4fbd51c0 100644 --- a/regression/cbmc-java/lazyloading9/test.desc +++ b/regression/cbmc-java/lazyloading9/test.desc @@ -1,6 +1,6 @@ CORE test.class ---lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point "test.*" +--lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point 'test.*' ^EXIT=0$ ^SIGNAL=0$ VERIFICATION SUCCESSFUL diff --git a/regression/cbmc-java/static_method1/test.desc b/regression/cbmc-java/static_method1/test.desc index c26f4061d02..2881b8787ce 100644 --- a/regression/cbmc-java/static_method1/test.desc +++ b/regression/cbmc-java/static_method1/test.desc @@ -1,6 +1,6 @@ CORE static_method1.class ---function "static_method1.f" --div-by-zero-check +--function 'static_method1.f' --div-by-zero-check ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc-java/swap2/test.desc b/regression/cbmc-java/swap2/test.desc index a7953d29a8b..69f2f769e40 100644 --- a/regression/cbmc-java/swap2/test.desc +++ b/regression/cbmc-java/swap2/test.desc @@ -1,6 +1,6 @@ CORE org/springframework/build/gradle/MergePlugin$1$_execute_closure1$_closure2.class ---function "org.springframework.build.gradle.MergePlugin\$1\$_execute_closure1\$_closure2.\$getCallSiteArray:()[Lorg/codehaus/groovy/runtime/callsite/CallSite;" +--function 'org.springframework.build.gradle.MergePlugin$1$_execute_closure1$_closure2.$getCallSiteArray:()[Lorg/codehaus/groovy/runtime/callsite/CallSite;' ^EXIT=0 ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc/Makefile b/regression/cbmc/Makefile index 9a14abc905f..486a8c750f7 100644 --- a/regression/cbmc/Makefile +++ b/regression/cbmc/Makefile @@ -1,16 +1,10 @@ default: tests.log test: - @if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \ - ../failed-tests-printer.pl ; \ - exit 1 ; \ - fi + @../test.pl -p -c ../../../src/cbmc/cbmc tests.log: ../test.pl - @if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \ - ../failed-tests-printer.pl ; \ - exit 1 ; \ - fi + @../test.pl -p -c ../../../src/cbmc/cbmc show: @for dir in *; do \ diff --git a/regression/cpp-linter/Makefile b/regression/cpp-linter/Makefile index 097b463fce5..7f537735d18 100644 --- a/regression/cpp-linter/Makefile +++ b/regression/cpp-linter/Makefile @@ -1,16 +1,10 @@ default: tests.log test: - @if ! ../test.pl -c python ../../../scripts/cpplint.py ; then \ - ../failed-tests-printer.pl ; \ - exit 1 ; \ - fi + @../test.pl -p -c "python ../../../scripts/cpplint.py" tests.log: ../test.pl - @if ! ../test.pl -c "python ../../../scripts/cpplint.py" ; then \ - ../failed-tests-printer.pl ; \ - exit 1 ; \ - fi + @../test.pl -p -c "python ../../../scripts/cpplint.py" show: @for dir in *; do \ diff --git a/regression/cpp/Makefile b/regression/cpp/Makefile index c770b3b3ed7..3146b15f028 100644 --- a/regression/cpp/Makefile +++ b/regression/cpp/Makefile @@ -10,16 +10,10 @@ else endif test: - @if ! ../test.pl -c $(exe) ; then \ - ../failed-tests-printer.pl ; \ - exit 1 ; \ - fi + @../test.pl -p -c $(exe) tests.log: ../test.pl - @if ! ../test.pl -c $(exe) ; then \ - ../failed-tests-printer.pl ; \ - exit 1 ; \ - fi + @../test.pl -p -c $(exe) show: @for dir in *; do \ diff --git a/regression/failed-tests-printer.pl b/regression/failed-tests-printer.pl deleted file mode 100755 index aa5f28b5933..00000000000 --- a/regression/failed-tests-printer.pl +++ /dev/null @@ -1,32 +0,0 @@ -#!/usr/bin/perl -w - -use strict; - -open LOG,") { - chomp; - if (/^Test '(.+)'/) { - $current_test = $1; - $printed_this_test = 0; - } elsif (/Descriptor:\s+([^\s]+)/) { - $descriptor_file = $1; - } elsif (/Output:\s+([^\s]+)/) { - $output_file = $1; - } elsif (/\[FAILED\]\s*$/) { - if(0 == $printed_this_test) { - $printed_this_test = 1; - print "\n\n"; - print "Failed test: $current_test\n"; - system("cat $current_test/$output_file"); - print "\n\nFailed $descriptor_file lines:\n"; - } - print "$_\n"; - } -} - diff --git a/regression/fault-localization/Makefile b/regression/fault-localization/Makefile index 9a14abc905f..486a8c750f7 100644 --- a/regression/fault-localization/Makefile +++ b/regression/fault-localization/Makefile @@ -1,16 +1,10 @@ default: tests.log test: - @if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \ - ../failed-tests-printer.pl ; \ - exit 1 ; \ - fi + @../test.pl -p -c ../../../src/cbmc/cbmc tests.log: ../test.pl - @if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \ - ../failed-tests-printer.pl ; \ - exit 1 ; \ - fi + @../test.pl -p -c ../../../src/cbmc/cbmc show: @for dir in *; do \ diff --git a/regression/goto-analyzer-taint/Makefile b/regression/goto-analyzer-taint/Makefile index ca7e7707afe..462e051669c 100644 --- a/regression/goto-analyzer-taint/Makefile +++ b/regression/goto-analyzer-taint/Makefile @@ -1,16 +1,10 @@ default: tests.log test: - @if ! ../test.pl -c ../../../src/goto-analyzer/goto-analyzer ; then \ - ../failed-tests-printer.pl ; \ - exit 1 ; \ - fi + @../test.pl -p -c ../../../src/goto-analyzer/goto-analyzer tests.log: ../test.pl - @if ! ../test.pl -c ../../../src/goto-analyzer/goto-analyzer ; then \ - ../failed-tests-printer.pl ; \ - exit 1 ; \ - fi + @../test.pl -p -c ../../../src/goto-analyzer/goto-analyzer show: @for dir in *; do \ diff --git a/regression/goto-analyzer/Makefile b/regression/goto-analyzer/Makefile index ca7e7707afe..462e051669c 100644 --- a/regression/goto-analyzer/Makefile +++ b/regression/goto-analyzer/Makefile @@ -1,16 +1,10 @@ default: tests.log test: - @if ! ../test.pl -c ../../../src/goto-analyzer/goto-analyzer ; then \ - ../failed-tests-printer.pl ; \ - exit 1 ; \ - fi + @../test.pl -p -c ../../../src/goto-analyzer/goto-analyzer tests.log: ../test.pl - @if ! ../test.pl -c ../../../src/goto-analyzer/goto-analyzer ; then \ - ../failed-tests-printer.pl ; \ - exit 1 ; \ - fi + @../test.pl -p -c ../../../src/goto-analyzer/goto-analyzer show: @for dir in *; do \ diff --git a/regression/goto-cc-cbmc/Makefile b/regression/goto-cc-cbmc/Makefile index 11ce6deb0ca..ce1f110cb49 100644 --- a/regression/goto-cc-cbmc/Makefile +++ b/regression/goto-cc-cbmc/Makefile @@ -5,23 +5,17 @@ include ../../src/common ifeq ($(BUILD_ENV_),MSVC) exe=../../../src/goto-cc/goto-cl - is_windows="true" + is_windows=true else exe=../../../src/goto-cc/goto-cc - is_windows="false" + is_windows=false endif test: - @if ! ../test.pl -c '../chain.sh $(exe) ../../../src/cbmc/cbmc $(is_windows)' ; then \ - ../failed-tests-printer.pl ; \ - exit 1; \ - fi + @../test.pl -p -c '../chain.sh $(exe) ../../../src/cbmc/cbmc $(is_windows)' tests.log: - @if ! ../test.pl -c '../chain.sh $(exe) ../../../src/cbmc/cbmc $(is_windows)' ; then \ - ../failed-tests-printer.pl ; \ - exit 1; \ - fi + @../test.pl -p -c '../chain.sh $(exe) ../../../src/cbmc/cbmc $(is_windows)' show: @for dir in *; do \ diff --git a/regression/goto-cc-cbmc/regenerate-entry-function/test.desc b/regression/goto-cc-cbmc/regenerate-entry-function/test.desc index ced965563f8..1ee374f196c 100644 --- a/regression/goto-cc-cbmc/regenerate-entry-function/test.desc +++ b/regression/goto-cc-cbmc/regenerate-entry-function/test.desc @@ -1,6 +1,6 @@ CORE main.c -"--function fun --cover branch" +'--function fun --cover branch' ^EXIT=0$ ^SIGNAL=0$ ^x= diff --git a/regression/goto-cc-goto-analyzer/Makefile b/regression/goto-cc-goto-analyzer/Makefile index 7f62e471b48..d0cf4b6b2da 100644 --- a/regression/goto-cc-goto-analyzer/Makefile +++ b/regression/goto-cc-goto-analyzer/Makefile @@ -5,24 +5,18 @@ include ../../src/common ifeq ($(BUILD_ENV_),MSVC) exe=../../../src/goto-cc/goto-cl - is_windows="true" + is_windows=true else exe=../../../src/goto-cc/goto-cc - is_windows="false" + is_windows=false endif test: - @if ! ../test.pl -c '../chain.sh $(exe) ../../../src/goto-analyzer/goto-analyzer $(is_windows)' ; then \ - ../failed-tests-printer.pl ; \ - exit 1; \ - fi + @../test.pl -p -c '../chain.sh $(exe) ../../../src/goto-analyzer/goto-analyzer $(is_windows)' tests.log: pwd - @if ! ../test.pl -c '../chain.sh $(exe) ../../../src/goto-analyzer/goto-analyzer $(is_windows)' ; then \ - ../failed-tests-printer.pl ; \ - exit 1; \ - fi + @../test.pl -p -c '../chain.sh $(exe) ../../../src/goto-analyzer/goto-analyzer $(is_windows)' show: @for dir in *; do \ diff --git a/regression/goto-cc-goto-analyzer/regenerate-entry-function/test.desc b/regression/goto-cc-goto-analyzer/regenerate-entry-function/test.desc index 0dd59956634..6e48067136c 100644 --- a/regression/goto-cc-goto-analyzer/regenerate-entry-function/test.desc +++ b/regression/goto-cc-goto-analyzer/regenerate-entry-function/test.desc @@ -1,6 +1,6 @@ CORE main.c -"--function fun --show-goto-functions" +'--function fun --show-goto-functions' ^\s*fun\(x\);$ ^EXIT=6$ ^SIGNAL=0$ diff --git a/regression/goto-diff/Makefile b/regression/goto-diff/Makefile index 266f02032bb..def628d35ff 100644 --- a/regression/goto-diff/Makefile +++ b/regression/goto-diff/Makefile @@ -1,16 +1,10 @@ default: tests.log test: - @if ! ../test.pl -c ../../../src/goto-diff/goto-diff ; then \ - ../failed-tests-printer.pl ; \ - exit 1 ; \ - fi + @../test.pl -p -c ../../../src/goto-diff/goto-diff tests.log: ../test.pl - @if ! ../test.pl -c ../../../src/goto-diff/goto-diff ; then \ - ../failed-tests-printer.pl ; \ - exit 1 ; \ - fi + @../test.pl -p -c ../../../src/goto-diff/goto-diff show: @for dir in *; do \ diff --git a/regression/goto-gcc/CMakeLists.txt b/regression/goto-gcc/CMakeLists.txt new file mode 100644 index 00000000000..47bc31b4a76 --- /dev/null +++ b/regression/goto-gcc/CMakeLists.txt @@ -0,0 +1,4 @@ +# TARGET_FILE (as used in other directories) can't be used with goto-gcc as it +# isn't marked as an executable (target), which CMake requires. Thus construct a +# path in the same way the symbolic link is created in the goto-cc directory. +add_test_pl_tests("$/goto-gcc") diff --git a/regression/goto-gcc/Makefile b/regression/goto-gcc/Makefile index c845d7e2e2a..e7838b58131 100644 --- a/regression/goto-gcc/Makefile +++ b/regression/goto-gcc/Makefile @@ -2,17 +2,11 @@ default: tests.log test: -@ln -s goto-cc ../../src/goto-cc/goto-gcc - @if ! ../test.pl -c ../../../src/goto-cc/goto-gcc ; then \ - ../failed-tests-printer.pl ; \ - exit 1 ; \ - fi + @../test.pl -p -c ../../../src/goto-cc/goto-gcc tests.log: ../test.pl -@ln -s goto-cc ../../src/goto-cc/goto-gcc - @if ! ../test.pl -c ../../../src/goto-cc/goto-gcc ; then \ - ../failed-tests-printer.pl ; \ - exit 1 ; \ - fi + @../test.pl -p -c ../../../src/goto-cc/goto-gcc show: @for dir in *; do \ diff --git a/regression/goto-instrument-typedef/Makefile b/regression/goto-instrument-typedef/Makefile index 56de781ae2c..45cd0b00b64 100644 --- a/regression/goto-instrument-typedef/Makefile +++ b/regression/goto-instrument-typedef/Makefile @@ -5,23 +5,17 @@ include ../../src/common ifeq ($(BUILD_ENV_),MSVC) exe=../../../src/goto-cc/goto-cl - is_windows="true" + is_windows=true else exe=../../../src/goto-cc/goto-cc - is_windows="false" + is_windows=false endif test: - @if ! ../test.pl -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument $(is_windows)' ; then \ - ../failed-tests-printer.pl ; \ - exit 1; \ - fi + @../test.pl -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument $(is_windows)' tests.log: - @if ! ../test.pl -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument $(is_windows)' ; then \ - ../failed-tests-printer.pl ; \ - exit 1; \ - fi + @../test.pl -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument $(is_windows)' show: @for dir in *; do \ diff --git a/regression/goto-instrument-typedef/typedef-anon-struct1/test.desc b/regression/goto-instrument-typedef/typedef-anon-struct1/test.desc index 59aba0e01a6..9fe8148da9b 100644 --- a/regression/goto-instrument-typedef/typedef-anon-struct1/test.desc +++ b/regression/goto-instrument-typedef/typedef-anon-struct1/test.desc @@ -1,6 +1,6 @@ CORE main.c -"--show-symbol-table" +--show-symbol-table // Enable multi-line checking activate-multi-line-match EXIT=0 diff --git a/regression/goto-instrument-typedef/typedef-anon-struct2/test.desc b/regression/goto-instrument-typedef/typedef-anon-struct2/test.desc index 490b6cc2623..7bc8b436b0c 100644 --- a/regression/goto-instrument-typedef/typedef-anon-struct2/test.desc +++ b/regression/goto-instrument-typedef/typedef-anon-struct2/test.desc @@ -1,6 +1,6 @@ CORE main.c -"--show-symbol-table" +--show-symbol-table // Enable multi-line checking activate-multi-line-match EXIT=0 diff --git a/regression/goto-instrument-typedef/typedef-anon-union1/test.desc b/regression/goto-instrument-typedef/typedef-anon-union1/test.desc index 86caf078d6a..452ab96857d 100644 --- a/regression/goto-instrument-typedef/typedef-anon-union1/test.desc +++ b/regression/goto-instrument-typedef/typedef-anon-union1/test.desc @@ -1,6 +1,6 @@ CORE main.c -"--show-symbol-table" +--show-symbol-table // Enable multi-line checking activate-multi-line-match EXIT=0 diff --git a/regression/goto-instrument-typedef/typedef-anon-union2/test.desc b/regression/goto-instrument-typedef/typedef-anon-union2/test.desc index 8d8ca64aa93..06e8834765c 100644 --- a/regression/goto-instrument-typedef/typedef-anon-union2/test.desc +++ b/regression/goto-instrument-typedef/typedef-anon-union2/test.desc @@ -1,6 +1,6 @@ CORE main.c -"--show-symbol-table" +--show-symbol-table // Enable multi-line checking activate-multi-line-match EXIT=0 diff --git a/regression/goto-instrument-typedef/typedef-const-struct1/test.desc b/regression/goto-instrument-typedef/typedef-const-struct1/test.desc index a6aad1f799a..6108d3c748c 100644 --- a/regression/goto-instrument-typedef/typedef-const-struct1/test.desc +++ b/regression/goto-instrument-typedef/typedef-const-struct1/test.desc @@ -1,6 +1,6 @@ CORE main.c -"--show-symbol-table" +--show-symbol-table // Enable multi-line checking activate-multi-line-match EXIT=0 diff --git a/regression/goto-instrument-typedef/typedef-const-type1/test.desc b/regression/goto-instrument-typedef/typedef-const-type1/test.desc index 481b097653f..f42e33d48b3 100644 --- a/regression/goto-instrument-typedef/typedef-const-type1/test.desc +++ b/regression/goto-instrument-typedef/typedef-const-type1/test.desc @@ -1,6 +1,6 @@ CORE main.c -"--show-symbol-table" +--show-symbol-table // Enable multi-line checking activate-multi-line-match EXIT=0 diff --git a/regression/goto-instrument-typedef/typedef-const-union1/test.desc b/regression/goto-instrument-typedef/typedef-const-union1/test.desc index cd303b85195..5509eae3f86 100644 --- a/regression/goto-instrument-typedef/typedef-const-union1/test.desc +++ b/regression/goto-instrument-typedef/typedef-const-union1/test.desc @@ -1,6 +1,6 @@ CORE main.c -"--show-symbol-table" +--show-symbol-table // Enable multi-line checking activate-multi-line-match EXIT=0 diff --git a/regression/goto-instrument-typedef/typedef-param-anon-struct1/test.desc b/regression/goto-instrument-typedef/typedef-param-anon-struct1/test.desc index 537526b4422..6e7b1a7af86 100644 --- a/regression/goto-instrument-typedef/typedef-param-anon-struct1/test.desc +++ b/regression/goto-instrument-typedef/typedef-param-anon-struct1/test.desc @@ -1,6 +1,6 @@ CORE main.c -"--show-symbol-table" +--show-symbol-table // Enable multi-line checking activate-multi-line-match EXIT=0 diff --git a/regression/goto-instrument-typedef/typedef-param-anon-union1/test.desc b/regression/goto-instrument-typedef/typedef-param-anon-union1/test.desc index 270316982a3..eb410ddec88 100644 --- a/regression/goto-instrument-typedef/typedef-param-anon-union1/test.desc +++ b/regression/goto-instrument-typedef/typedef-param-anon-union1/test.desc @@ -1,6 +1,6 @@ CORE main.c -"--show-symbol-table" +--show-symbol-table // Enable multi-line checking activate-multi-line-match EXIT=0 diff --git a/regression/goto-instrument-typedef/typedef-param-struct1/test.desc b/regression/goto-instrument-typedef/typedef-param-struct1/test.desc index c26ee458459..c854c49f9d2 100644 --- a/regression/goto-instrument-typedef/typedef-param-struct1/test.desc +++ b/regression/goto-instrument-typedef/typedef-param-struct1/test.desc @@ -1,6 +1,6 @@ CORE main.c -"--show-symbol-table" +--show-symbol-table // Enable multi-line checking activate-multi-line-match EXIT=0 diff --git a/regression/goto-instrument-typedef/typedef-param-type1/test.desc b/regression/goto-instrument-typedef/typedef-param-type1/test.desc index 050ac22b315..983f133b00d 100644 --- a/regression/goto-instrument-typedef/typedef-param-type1/test.desc +++ b/regression/goto-instrument-typedef/typedef-param-type1/test.desc @@ -1,6 +1,6 @@ CORE main.c -"--show-symbol-table" +--show-symbol-table // Enable multi-line checking activate-multi-line-match EXIT=0 diff --git a/regression/goto-instrument-typedef/typedef-param-type2/test.desc b/regression/goto-instrument-typedef/typedef-param-type2/test.desc index 53cdc42193e..3ab0a4c870b 100644 --- a/regression/goto-instrument-typedef/typedef-param-type2/test.desc +++ b/regression/goto-instrument-typedef/typedef-param-type2/test.desc @@ -1,6 +1,6 @@ CORE main.c -"--show-symbol-table" +--show-symbol-table // Enable multi-line checking activate-multi-line-match EXIT=0 diff --git a/regression/goto-instrument-typedef/typedef-param-type3/test.desc b/regression/goto-instrument-typedef/typedef-param-type3/test.desc index 6ba9d61f8ca..647c157fafc 100644 --- a/regression/goto-instrument-typedef/typedef-param-type3/test.desc +++ b/regression/goto-instrument-typedef/typedef-param-type3/test.desc @@ -1,6 +1,6 @@ CORE main.c -"--show-symbol-table" +--show-symbol-table // Enable multi-line checking activate-multi-line-match EXIT=0 diff --git a/regression/goto-instrument-typedef/typedef-param-union1/test.desc b/regression/goto-instrument-typedef/typedef-param-union1/test.desc index 466dd76ed52..6bf1afdf628 100644 --- a/regression/goto-instrument-typedef/typedef-param-union1/test.desc +++ b/regression/goto-instrument-typedef/typedef-param-union1/test.desc @@ -1,6 +1,6 @@ CORE main.c -"--show-symbol-table" +--show-symbol-table // Enable multi-line checking activate-multi-line-match EXIT=0 diff --git a/regression/goto-instrument-typedef/typedef-return-anon-struct1/test.desc b/regression/goto-instrument-typedef/typedef-return-anon-struct1/test.desc index 47964f71f66..1cdd14e9ba4 100644 --- a/regression/goto-instrument-typedef/typedef-return-anon-struct1/test.desc +++ b/regression/goto-instrument-typedef/typedef-return-anon-struct1/test.desc @@ -1,6 +1,6 @@ CORE main.c -"--show-symbol-table" +--show-symbol-table // Enable multi-line checking activate-multi-line-match EXIT=0 diff --git a/regression/goto-instrument-typedef/typedef-return-anon-union1/test.desc b/regression/goto-instrument-typedef/typedef-return-anon-union1/test.desc index 5a8d1b2062d..94ce1ccc788 100644 --- a/regression/goto-instrument-typedef/typedef-return-anon-union1/test.desc +++ b/regression/goto-instrument-typedef/typedef-return-anon-union1/test.desc @@ -1,6 +1,6 @@ CORE main.c -"--show-symbol-table" +--show-symbol-table // Enable multi-line checking activate-multi-line-match EXIT=0 diff --git a/regression/goto-instrument-typedef/typedef-return-struct1/test.desc b/regression/goto-instrument-typedef/typedef-return-struct1/test.desc index eade5942ac8..fa9e7afb14c 100644 --- a/regression/goto-instrument-typedef/typedef-return-struct1/test.desc +++ b/regression/goto-instrument-typedef/typedef-return-struct1/test.desc @@ -1,6 +1,6 @@ CORE main.c -"--show-symbol-table" +--show-symbol-table // Enable multi-line checking activate-multi-line-match EXIT=0 diff --git a/regression/goto-instrument-typedef/typedef-return-type1/test.desc b/regression/goto-instrument-typedef/typedef-return-type1/test.desc index ba1b96ce6b6..efc8f8476ad 100644 --- a/regression/goto-instrument-typedef/typedef-return-type1/test.desc +++ b/regression/goto-instrument-typedef/typedef-return-type1/test.desc @@ -1,6 +1,6 @@ CORE main.c -"--show-symbol-table" +--show-symbol-table // Enable multi-line checking activate-multi-line-match EXIT=0 diff --git a/regression/goto-instrument-typedef/typedef-return-type2/test.desc b/regression/goto-instrument-typedef/typedef-return-type2/test.desc index 1ecc9ea8e90..28d7c3e1703 100644 --- a/regression/goto-instrument-typedef/typedef-return-type2/test.desc +++ b/regression/goto-instrument-typedef/typedef-return-type2/test.desc @@ -1,6 +1,6 @@ CORE main.c -"--show-symbol-table" +--show-symbol-table // Enable multi-line checking activate-multi-line-match EXIT=0 diff --git a/regression/goto-instrument-typedef/typedef-return-type3/test.desc b/regression/goto-instrument-typedef/typedef-return-type3/test.desc index 2401af3ce8d..2ce71940ee5 100644 --- a/regression/goto-instrument-typedef/typedef-return-type3/test.desc +++ b/regression/goto-instrument-typedef/typedef-return-type3/test.desc @@ -1,6 +1,6 @@ CORE main.c -"--show-symbol-table" +--show-symbol-table // Enable multi-line checking activate-multi-line-match EXIT=0 diff --git a/regression/goto-instrument-typedef/typedef-return-union1/test.desc b/regression/goto-instrument-typedef/typedef-return-union1/test.desc index 0855b28f479..33b17ca0c49 100644 --- a/regression/goto-instrument-typedef/typedef-return-union1/test.desc +++ b/regression/goto-instrument-typedef/typedef-return-union1/test.desc @@ -1,6 +1,6 @@ CORE main.c -"--show-symbol-table" +--show-symbol-table // Enable multi-line checking activate-multi-line-match EXIT=0 diff --git a/regression/goto-instrument-typedef/typedef-struct1/test.desc b/regression/goto-instrument-typedef/typedef-struct1/test.desc index 6a02f2d2174..51c56222053 100644 --- a/regression/goto-instrument-typedef/typedef-struct1/test.desc +++ b/regression/goto-instrument-typedef/typedef-struct1/test.desc @@ -1,6 +1,6 @@ CORE main.c -"--show-symbol-table" +--show-symbol-table // Enable multi-line checking activate-multi-line-match EXIT=0 diff --git a/regression/goto-instrument-typedef/typedef-struct2/test.desc b/regression/goto-instrument-typedef/typedef-struct2/test.desc index 6a02f2d2174..51c56222053 100644 --- a/regression/goto-instrument-typedef/typedef-struct2/test.desc +++ b/regression/goto-instrument-typedef/typedef-struct2/test.desc @@ -1,6 +1,6 @@ CORE main.c -"--show-symbol-table" +--show-symbol-table // Enable multi-line checking activate-multi-line-match EXIT=0 diff --git a/regression/goto-instrument-typedef/typedef-type1/test.desc b/regression/goto-instrument-typedef/typedef-type1/test.desc index 7599f1759c0..a70bad5d3f7 100644 --- a/regression/goto-instrument-typedef/typedef-type1/test.desc +++ b/regression/goto-instrument-typedef/typedef-type1/test.desc @@ -1,6 +1,6 @@ CORE main.c -"--show-symbol-table" +--show-symbol-table // Enable multi-line checking activate-multi-line-match EXIT=0 diff --git a/regression/goto-instrument-typedef/typedef-type2/test.desc b/regression/goto-instrument-typedef/typedef-type2/test.desc index 3cf1e50a5a5..f82d00237a5 100644 --- a/regression/goto-instrument-typedef/typedef-type2/test.desc +++ b/regression/goto-instrument-typedef/typedef-type2/test.desc @@ -1,6 +1,6 @@ CORE main.c -"--show-symbol-table" +--show-symbol-table // Enable multi-line checking activate-multi-line-match EXIT=0 diff --git a/regression/goto-instrument-typedef/typedef-type3/test.desc b/regression/goto-instrument-typedef/typedef-type3/test.desc index aca9069695c..077cec97390 100644 --- a/regression/goto-instrument-typedef/typedef-type3/test.desc +++ b/regression/goto-instrument-typedef/typedef-type3/test.desc @@ -1,6 +1,6 @@ CORE main.c -"--show-symbol-table" +--show-symbol-table // Enable multi-line checking activate-multi-line-match EXIT=0 diff --git a/regression/goto-instrument-typedef/typedef-type4/test.desc b/regression/goto-instrument-typedef/typedef-type4/test.desc index 28163714070..5e3fd8af85d 100644 --- a/regression/goto-instrument-typedef/typedef-type4/test.desc +++ b/regression/goto-instrument-typedef/typedef-type4/test.desc @@ -1,6 +1,6 @@ CORE main.c -"--show-symbol-table" +--show-symbol-table // Enable multi-line checking activate-multi-line-match EXIT=0 diff --git a/regression/goto-instrument-typedef/typedef-union1/test.desc b/regression/goto-instrument-typedef/typedef-union1/test.desc index 8502d149cb1..b4eab1b58e3 100644 --- a/regression/goto-instrument-typedef/typedef-union1/test.desc +++ b/regression/goto-instrument-typedef/typedef-union1/test.desc @@ -1,6 +1,6 @@ CORE main.c -"--show-symbol-table" +--show-symbol-table // Enable multi-line checking activate-multi-line-match EXIT=0 diff --git a/regression/goto-instrument-typedef/typedef-union2/test.desc b/regression/goto-instrument-typedef/typedef-union2/test.desc index 0fc908a6ab5..629a76f7bfb 100644 --- a/regression/goto-instrument-typedef/typedef-union2/test.desc +++ b/regression/goto-instrument-typedef/typedef-union2/test.desc @@ -1,6 +1,6 @@ CORE main.c -"--show-symbol-table" +--show-symbol-table // Enable multi-line checking activate-multi-line-match EXIT=0 diff --git a/regression/goto-instrument/Makefile b/regression/goto-instrument/Makefile index a8d54370285..8d53e0b2656 100644 --- a/regression/goto-instrument/Makefile +++ b/regression/goto-instrument/Makefile @@ -5,23 +5,17 @@ include ../../src/common ifeq ($(BUILD_ENV_),MSVC) exe=../../../src/goto-cc/goto-cl - is_windows="true" + is_windows=true else exe=../../../src/goto-cc/goto-cc - is_windows="false" + is_windows=false endif test: - @if ! ../test.pl -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)' ; then \ - ../failed-tests-printer.pl ; \ - exit 1; \ - fi + @../test.pl -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)' tests.log: - @if ! ../test.pl -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)' ; then \ - ../failed-tests-printer.pl ; \ - exit 1; \ - fi + @../test.pl -p -c '../chain.sh $(exe) ../../../src/goto-instrument/goto-instrument ../../../src/cbmc/cbmc $(is_windows)' show: @for dir in *; do \ diff --git a/regression/invariants/Makefile b/regression/invariants/Makefile index 96c4a9e8077..4fbc8a60aee 100644 --- a/regression/invariants/Makefile +++ b/regression/invariants/Makefile @@ -11,16 +11,10 @@ include ../../src/config.inc include ../../src/common test: driver$(EXEEXT) - @if ! ../test.pl -c ../driver ; then \ - ../failed-tests-printer.pl ; \ - exit 1 ; \ - fi + @../test.pl -p -c ../driver tests.log: ../test.pl driver$(EXEEXT) - @if ! ../test.pl -c ../driver ; then \ - ../failed-tests-printer.pl ; \ - exit 1 ; \ - fi + @../test.pl -p -c ../driver show: @for dir in *; do \ diff --git a/regression/strings-smoke-tests/Makefile b/regression/strings-smoke-tests/Makefile index e45465e6130..58058dbc77a 100644 --- a/regression/strings-smoke-tests/Makefile +++ b/regression/strings-smoke-tests/Makefile @@ -1,28 +1,16 @@ default: tests.log test: - @if ! ../test.pl -c ../../../src/jbmc/jbmc ; then \ - ../failed-tests-printer.pl ; \ - exit 1 ; \ - fi + @../test.pl -p -c ../../../src/jbmc/jbmc testfuture: - @if ! ../test.pl -c ../../../src/jbmc/jbmc -CF ; then \ - ../failed-tests-printer.pl ; \ - exit 1 ; \ - fi + @../test.pl -p -c ../../../src/jbmc/jbmc -CF testall: - @if ! ../test.pl -c ../../../src/jbmc/jbmc -CFTK ; then \ - ../failed-tests-printer.pl ; \ - exit 1 ; \ - fi + @../test.pl -p -c ../../../src/jbmc/jbmc -CFTK tests.log: ../test.pl - @if ! ../test.pl -c ../../../src/jbmc/jbmc ; then \ - ../failed-tests-printer.pl ; \ - exit 1 ; \ - fi + @../test.pl -p -c ../../../src/jbmc/jbmc show: @for dir in *; do \ diff --git a/regression/strings/Makefile b/regression/strings/Makefile index 47653a6bb95..522ddee5b25 100644 --- a/regression/strings/Makefile +++ b/regression/strings/Makefile @@ -1,28 +1,16 @@ default: tests.log test: - @if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \ - ../failed-tests-printer.pl ; \ - exit 1 ; \ - fi + @../test.pl -p -c ../../../src/cbmc/cbmc testfuture: - @if ! ../test.pl -c ../../../src/cbmc/cbmc -CF ; then \ - ../failed-tests-printer.pl ; \ - exit 1 ; \ - fi + @../test.pl -p -c ../../../src/cbmc/cbmc -CF testall: - @if ! ../test.pl -c ../../../src/cbmc/cbmc -CFTK ; then \ - ../failed-tests-printer.pl ; \ - exit 1 ; \ - fi + @../test.pl -p -c ../../../src/cbmc/cbmc -CFTK tests.log: ../test.pl - @if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \ - ../failed-tests-printer.pl ; \ - exit 1 ; \ - fi + @../test.pl -p -c ../../../src/cbmc/cbmc show: @for dir in *; do \ diff --git a/regression/test-script/Makefile b/regression/test-script/Makefile index ee6eaf02884..f0b67581e9f 100644 --- a/regression/test-script/Makefile +++ b/regression/test-script/Makefile @@ -2,31 +2,19 @@ default: tests.log test: - @if ! ../test.pl -c ../program_runner.sh ; then \ - ../failed-tests-printer.pl ; \ - exit 1; \ - fi + @../test.pl -p -c ../program_runner.sh @echo "Testing KNOWNBUG fail" - @if ! ../test.pl -c ../program_runner.sh -K ; then \ - ../failed-tests-printer.pl ; \ - exit 1; \ - fi + @../test.pl -p -c ../program_runner.sh -K tests.log: pwd - @if ! ../test.pl -c ../program_runner.sh ; then \ - ../failed-tests-printer.pl ; \ - exit 1; \ - fi + @../test.pl -p -c ../program_runner.sh @echo "Testing KNOWNBUG fail" - @if ! ../test.pl -c ../program_runner.sh -K ; then \ - ../failed-tests-printer.pl ; \ - exit 1; \ - fi + @../test.pl -p -c ../program_runner.sh -K show: @for dir in *; do \ diff --git a/regression/test.pl b/regression/test.pl index 41d659ee96d..8cd558feafd 100755 --- a/regression/test.pl +++ b/regression/test.pl @@ -42,8 +42,10 @@ ($$$$$) } } - system "echo EXIT=$exit_value >>'$name/$output'"; - system "echo SIGNAL=$signal_num >>'$name/$output'"; + open my $FH, ">>$name/$output"; + print $FH "EXIT=$exit_value\n"; + print $FH "SIGNAL=$signal_num\n"; + close $FH; if($signal_num == 2) { print "\nProgram under test interrupted; stopping\n"; @@ -234,6 +236,7 @@ ($$$$) -i options in test.desc matching the specified perl regex are ignored -j run tests in parallel (requires Thread::Pool::Simple) -n dry-run: print the tests that would be run, but don't actually run them + -p print logs of each failed test (if any) -h show this help and exit -C core: run all essential tests (default if none of C/T/F/K are given) -T thorough: run expensive tests @@ -275,10 +278,10 @@ ($$$$) use Getopt::Long qw(:config pass_through bundling); $main::VERSION = 0.1; $Getopt::Std::STANDARD_HELP_VERSION = 1; -our ($opt_c, $opt_i, $opt_j, $opt_n, $opt_h, $opt_C, $opt_T, $opt_F, $opt_K, %defines); # the variables for getopt +our ($opt_c, $opt_i, $opt_j, $opt_n, $opt_p, $opt_h, $opt_C, $opt_T, $opt_F, $opt_K, %defines); # the variables for getopt $opt_j = 0; GetOptions("D=s", \%defines); -getopts('c:i:j:nhCTFK') or &main::HELP_MESSAGE(\*STDOUT, "", $main::VERSION, ""); +getopts('c:i:j:nphCTFK') or &main::HELP_MESSAGE(\*STDOUT, "", $main::VERSION, ""); $opt_c or &main::HELP_MESSAGE(\*STDOUT, "", $main::VERSION, ""); (!$opt_j || $has_thread_pool) or &main::HELP_MESSAGE(\*STDOUT, "", $main::VERSION, ""); $opt_h and &main::HELP_MESSAGE(\*STDOUT, "", $main::VERSION, ""); @@ -371,4 +374,41 @@ ($) close LOG; +if($opt_p && $failures != 0) { + open LOG,") { + chomp $line; + if ($line =~ /^Test '(.+)'/) { + $current_test = $1; + $printed_this_test = 0; + } elsif ($line =~ /Descriptor:\s+([^\s]+)/) { + $descriptor_file = $1; + } elsif ($line =~ /Output:\s+([^\s]+)/) { + $output_file = $1; + } elsif ($line =~ /\[FAILED\]\s*$/) { + # print a descriptive header before dumping the test.desc lines that + # actually weren't matched (and print this header just once) + if(0 == $printed_this_test) { + $printed_this_test = 1; + print "\n\n"; + print "Failed test: $current_test\n"; + open FH, "<$current_test/$output_file"; + while (my $f = ) { + print $f; + } + close FH; + print "\n\nFailed $descriptor_file lines:\n"; + } + + print "$line\n"; + } + } +} + exit $failures; diff --git a/src/goto-cc/CMakeLists.txt b/src/goto-cc/CMakeLists.txt index 7d7a2d579da..8508fb6924d 100644 --- a/src/goto-cc/CMakeLists.txt +++ b/src/goto-cc/CMakeLists.txt @@ -29,4 +29,9 @@ target_link_libraries(goto-cc goto-cc-lib) if(WIN32) set_target_properties(goto-cc PROPERTIES OUTPUT_NAME goto-cl) +else() + add_custom_command(TARGET goto-cc + POST_BUILD + COMMAND "${CMAKE_COMMAND}" -E create_symlink + goto-cc $/goto-gcc) endif()