[Termtools] Technical Problems with AProVE (C Category)

[Jera Hensel]

Dear all,

unfortunately, there were some technical problems concerning the
interaction of Starexec and our tool AProVE in the C category.

- Starexec merges stderr and stdout. Usually, we redirect stderr to
/dev/null to deal with this issue. This redirection was missing in our
configuration for the C category. Hence, Starexec interpreted e.g. clang
warnings as invalid results.
- Since AProVE depends on a specific version of Clang, which is not
available on Starexec, we bundled AProVE with the required version of
Clang and stripped down versions of standard library headers.
Unfortunately, size_t and NULL were missing in our stripped down version
of stdlib.h, such that Clang could not compile examples that use size_t
or NULL.

Hence, AProVE failed on several examples which are easily solved by the
AProVE-binary used for the competition on a usual linux system with the
required version of Clang. For that reason, we think that the results in
the C category do not fully allow a comparison of tools for termination
analysis of C programs. As a result, we want to propose a rerun of the C
category, although we know that we could (and should) have fixed these
issues prior to the competition.

Best regards,
Jera