I have concluded (hopefully not erroneously) that I have failed to properly
constructed either llvm or KLEE or both of (KLEE and llvm)
This conclusion is based on the test problem
int test(int a)
{
if ((a < 1) || (a > 1) )
return 1;
else
return 0;
}
The example is so trivial, that it can't possibly be the algorithms of
either llvm or KLEE.
The clause partitions the integer domain into 3 equivalence classes.
2 - (a < 1) and (a > 1) - map to a return of 1;
1 - (a = 1) - maps to a return of 0;
I only got 2 test cases.
a = 0
a = 2
This is perplexing to me, as I have run the 3 tutorials, and believe the
results to be consistent with the tutorial web page.
dbl
