[Termtools] Technical Problems with AProVE (C Category)

[Matthias Heizmann]

Hi all,

> we want to propose a rerun of the C category,
I'm fine with it. 
(I represent one of the competing teams in this category.)

Matthias


On Thursday, August 06, 2015 09:35:56 Jera Hensel wrote:
> 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
> _______________________________________________
> Termtools mailing list
> Termtools at lists.lri.fr
> http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: This is a digitally signed message part.
URL: <http://lists.lri.fr/pipermail/termtools/attachments/20150806/6667c680/attachment.sig>