I have started to play with Klee to see what it does, to see its limits
The test problem which I choose to apply first 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 a bit weak
a = 0;
a = 2;
the search clauses were probably
(for a = 0) find a such that a < 1
(for a = 2) find a such that not (a < 1)
The goal appears to be equivalence class test case generation
The search clauses probably should have been
find maximal a such that a < 1
find minimal a such that not ( a < 1)
The ration for this believe - equivalence class testing in not adequate, the
edges of the equivalence class need to be examined. For integer valued
quantities, this is the off by one phenomena (i.e. coding <= x instead of <
x)
dbl
