Skip to content

Merge failed-tests-printer and enable in CMake #1502

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 6 commits into from
Nov 2, 2017
Merged

Merge failed-tests-printer and enable in CMake #1502

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
96e169a
Use single quotes for Windows compatibility
tautschnig Oct 25, 2017
ba16006
Do not use shell built-ins
tautschnig Oct 24, 2017
3321735
Move implementation of failed-tests-printer.pl into test.pl
tautschnig Oct 19, 2017
dd6e431
test.pl: Use native perl instead of "cat" to print log file
tautschnig Oct 20, 2017
6016bef
Improve readability of code imported from failed-tests-printer.pl
tautschnig Nov 1, 2017
4b0e2d4
Create goto-gcc symlink in cmake builds and enable goto-gcc tests
tautschnig Oct 19, 2017
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 4 additions & 1 deletion regression/CMakeLists.txt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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)
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This will fail, as there is no CMakeLists.txt in goto-gcc. If you add a file with the following contents, it should work though:

add_test_pl_tests(
    "$<TARGET_FILE:goto-gcc>"
)

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you for the guidance! I've added this in 4a5dff1 and will squash once CI succeeds.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Think I got this wrong - if goto-gcc isn't a target, then we can't find its path in this way. As an alternative, I would hard-code the goto-gcc symlink location as ${CMAKE_BINARY_DIR}/goto-gcc, and then use that path as the argument to add_test_pl_tests

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've now gone for cb9f586 - I feels like a horrible hack, but I haven't managed to figure out a way of marking a symlink as "executable". Maybe your hard-coded approach is the better option?

endif()
add_subdirectory(invariants)
add_subdirectory(jbmc-strings)
add_subdirectory(strings)
Expand Down
10 changes: 2 additions & 8 deletions regression/ansi-c/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 \
Expand Down
10 changes: 2 additions & 8 deletions regression/cbmc-cover/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 \
Expand Down
10 changes: 2 additions & 8 deletions regression/cbmc-java-inheritance/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 \
Expand Down
10 changes: 2 additions & 8 deletions regression/cbmc-java/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 \
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-java/classpath2/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-java/function1/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
Main.class
--function "Other.fail:()V"
--function 'Other.fail:()V'
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-java/function2/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
Main.class
--function "D.fail:()V"
--function 'D.fail:()V'
^EXIT=10$
^SIGNAL=0$
^VERIFICATION FAILED$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-java/function3/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
KNOWNBUG
Main.class
--function "A.dummy:()V"
--function 'A.dummy:()V'
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-java/function4/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
KNOWNBUG
Main.class
--function "Other.fail"
--function 'Other.fail'
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-java/jar-file4/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-java/lazyloading11/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-java/lazyloading7/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-java/lazyloading8/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-java/lazyloading9/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-java/static_method1/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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$
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-java/swap2/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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;'
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm in relative awe at you tracking this down btw, glad we found a combination of escaped characters and quotes that is cross platform compatible...

^EXIT=0
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
Expand Down
10 changes: 2 additions & 8 deletions regression/cbmc/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 \
Expand Down
10 changes: 2 additions & 8 deletions regression/cpp-linter/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 \
Expand Down
10 changes: 2 additions & 8 deletions regression/cpp/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 \
Expand Down
32 changes: 0 additions & 32 deletions regression/failed-tests-printer.pl
View file
Open in desktop

This file was deleted.

10 changes: 2 additions & 8 deletions regression/fault-localization/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 \
Expand Down
10 changes: 2 additions & 8 deletions regression/goto-analyzer-taint/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 \
Expand Down
10 changes: 2 additions & 8 deletions regression/goto-analyzer/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 \
Expand Down
14 changes: 4 additions & 10 deletions regression/goto-cc-cbmc/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 \
Expand Down
2 changes: 1 addition & 1 deletion regression/goto-cc-cbmc/regenerate-entry-function/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
CORE
main.c
"--function fun --cover branch"
'--function fun --cover branch'
^EXIT=0$
^SIGNAL=0$
^x=
Expand Down
Loading