Some of the system tests fail

[davidtr1037]

Some of the tests related to ubsan runtime fail when running: make check (or make systemtests).
It seems that debug information is missing and as a result, the log messages are different from those that are expected.
For example:

KLEE: ERROR: (location information missing) load invalid value

Are some specific compilation flags needed in order to run make check?

Run: make check

The output can be seen when running the command from above.

Running on Ubuntu 22.04 with:

• GCC 11.4.0
• LLVM 13.0.0 (compiled from sources)

[jbuening]

@davidtr1037 I guess you used KLEE_RUNTIME_BUILD_TYPE=Release or something similar when you compiled KLEE?

The failing tests actually rely on debug info to be present in the (UBSan) runtime---and not, as in many other cases, the compilation unit of the test itself. See #1611 for a suggestion to avoid the test failures (patching the tests to use a different runtime build). Note that for some time already, KLEE's build system builds more than just the specified KLEE_RUNTIME_BUILD_TYPE (#1250), since then this variable (more or less?) just controls the default for -runtime-build.

[davidtr1037]

Thanks!