goto-gcc tests don't work under CMake

[thk123]

The regression tests in goto-gcc are not enabled on CMake (#1481 tried to turn them on).

Travis build output:

53: Test command: /home/travis/build/diffblue/cbmc/regression/test.pl "-c" "/home/travis/build/diffblue/cbmc/build/bin/goto-cc" "-C"
53: Test timeout computed to be: 9.99988e+06
53: Loading
53:   5 tests found
53: 
53: Running tests
53:   Running expect_fail/test.desc  [FAILED]
53:   Running ignore_cprover_macros/test.desc  [OK]
53:   Running run_diagnostic/test.desc  [FAILED]
53:   Running verbosity1/test.desc  [OK]
53:   Running verbosity2/test.desc  [FAILED]
53: 
53: Tests failed
53:   3 of 5 tests failed
17/23 Test #53: goto-gcc-CORE ....................***Failed    1.40 sec

https://travis-ci.org/diffblue/cbmc/jobs/289820097

[tautschnig]

It seems the CMake test runs don't output details in case of failure? Does the CMake set up do (some equivalent of) ln -s goto-cc ../../src/goto-cc/goto-gcc? @reuk could something be done about the first question of mine here?

[reuk]

At the moment, the makefiles run the test.pl script, and run a second script to print output if the first script fails. CMake only allows us to run a single command for each test, so I would recommend either:

• Adding a flag to the test.pl script which automatically prints output on failure, or
• Writing a wrapper script for test.pl + the failed-test-printer.

[tautschnig]

Question by a CMake dummy:

CMake only allows us to run a single command for each test

Does that mean that test.pl <options> || failed-tests-printer.pl is not possible?

Either way it might be a good idea to integrate the printer into test.pl

[reuk]

Yes, it has to be a single cmd arg0 arg1 arg2 invocation. The command isn't run in a shell, so binops like || won't work.

I think adding an option to test.pl to print failed tests is probably the best way forward, as this will simplify the makefiles too. However, I don't know any Perl so unfortunately I won't be able to make this change myself.

[tautschnig]

I'm taking care of the failed-tests-printer integration. @reuk Could you advise on how to run ln -s goto-cc ../../src/goto-cc/goto-gcc (well, some equivalent of it in the right folder) as part of src/goto-cc/CMakeLists.txt when not on Windows?

[reuk]

I don't understand the significance of the symlink here. Why can't these tests be run with goto-cc directly?

[tautschnig]

The behaviour of goto-cc varies according to the name that it has been invoked as. (Hence also the goto-cc -> goto-cl renaming on Windows.)

[reuk]

Cmake has some built-in portable command which you can see with cmake -E.

To run them from a custom_command you would do something like ${CMAKE_COMMAND} -E create_symlink <$TARGET_FILE:goto-cc> goto-gcc.

The actual custom_command should probably be a post-build command on goto-cc: https://cmake.org/cmake/help/v3.0/command/add_custom_command.html

[tautschnig]

Thanks @reuk! I've tried to translate this into code in #1502.