[Termtools] TPDB -- C-Integer Complexity

[Florian Frohn]

Dear all,

during the preparations for the upcoming TermComp I came across some
oddities regarding the category "C-Integer Complexity". First of all,
the TPDB contains just 26 examples for this category, but according to
the Call for Participation at least 40 examples are required. More
importantly, they do not conform to the TermComp definition of C-Integer
programs (http://www.termination-portal.org/wiki/C_Integer_Programs).
E.g., cBench_bin_search_StepSize2.c uses "nondet" instead of
"__VERIFIER_nondet_int" for nondeterminism and it uses division, which
is not allowed by the definition.

Assuming that we agree on the definition from
http://www.termination-portal.org/wiki/C_Integer_Programs (which was
discussed when the category "C-Integer Termination" was introduced), I
propose to

1. remove all examples that do not conform to the definition,
2. collect new examples, and
3. use the examples from "C-Integer Termination" as fallback (i.e., if
less than 40 examples are submitted), even though some of them might be
uninteresting for complexity analysis.

What do the other participants of this category think?

Best
Florian


PS: Sorry if you received multiple copies of this mail, there were some
technical issues.