I have started to play with Klee to see what it does, to see its limits
The test problem which I choose to apply second was
int test(int a)
{
if (a == 1)
return 1;
else
return 0;
}
Path coverage was achieved. No question about it.
The selected test cases generated were incomplete (personal opinion, reason
provided below)
a = 0;
a = 3;
the search clauses were probably
(for a = 0) find a such that a == 1
(for a = 3) find a such that not (a == 1)
The integers are an ordered set.
The preferred value established by the clause (a == 1) establishes 3
equivalence classes
(1) a < 1
(2) a == 1
(3) 1 < a
I would expect to see a case from each equivalence class
The rational for the 3 classes is to establish that a particular class of
coding errors is absent. (inappropriate choice of the comparison operator)
In this case either
(a) substituting <= for ==
(b) substituting >= for ==
(c) substituting > for ==
(d) substitution < for ==
One would like to believe that the software developer doesn't make such
mistakes, but it happens. More importantly when execution time becomes
critical occasionally someone will optimize using an assembly procedure.
Assembly is much more prone to such mistakes.
It is not clear to be whether these kind of issues are in scope or out of
scope (given the intended class of problems which are intended to be
addressed).
dbl
