[Termtools] Technical Problems with AProVE (C Category)

[Ton-Chanh Le]

Hi all,

We, the team HipTNT+ in this category, are also fine with the rerun.
On Aug 6, 2015 6:28 PM, "Matthias Heizmann" <
heizmann at informatik.uni-freiburg.de> wrote:

> 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
>
> _______________________________________________
> Termtools mailing list
> Termtools at lists.lri.fr
> http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.lri.fr/pipermail/termtools/attachments/20150807/0f7b7727/attachment.html>