[Termtools] TermComp test runs C Integer Termination

[Florian Frohn]

Dear all,

there's something strange going on in the test runs for C Integer
Termination. It seems like the only defined function in the
test-examples is called "foo", see:

https://termcomp.imn.htwk-leipzig.de/pairs/304320076 (UBA, 'Found
specification of procedure foo')
https://termcomp.imn.htwk-leipzig.de/pairs/304320075 (AProVE,
'BasicFunctionTypename: "foo"')

However, according to the rules for the category, it should be "main"
(see http://termination-portal.org/wiki/C_Integer_Programs), which is
the case for the corresponding TPDB examples (see, e.g.,
http://cl2-informatik.uibk.ac.at/mercurial.cgi/TPDB/file/3ce4bce287e1/C_Integer/Stroeder_15/GulavaniGulwani-CAV2008-Fig1c_true-termination.c).

Unless an entry point is specified explicitly, AProVE always tries to
analyze main. Since no such function exists, AProVE currently fails for
all examples in the test runs.

Which examples are currently used for testing and which examples will be
used for the competition?

Best
Florian