I hope to use Klee to help me in generating test cases, and I have met some
problems.
When the symbolic variable appears in the offset of a pointer or an array, such
as:
int *p;
int b[3];
int x;
klee_make_symbolic(&x,sizeof(x),"x");
if (p[x] > 3){...}
if (b[x] > 3){...}
for (int i = 0;i < x;i++){ p[i] ... }
during the symbolic execution,it always occurs error like "out of bound
pointer",
And the value of x that solved by klee also is greater than the size of the
pointer or array.
If the pointer is allocated memory by a sized array, such as:
p = b;
How can I make sure that the symbolic variable x is restricted from 0-2 ?
I have an idea that when I fix with the gep instruction in
executeInstruction(), if the offset is not a constantexpr and the geptype has
<ArrayType>, I append two constraints that x >=0 and x < sizeof(b).So
that the symbolic value x will not be out of bound.This can solve the problem
of array,but I do not know how to fix pointer.
If the pointer is allocates memory by a sized array(int *p = b),I hope that the
offset should be restricted from 0 to the size of the array, but when I fix
with the gep instruction(p[x]),I cannot get the size of the array.I only know
the pointer type and the size of the type from the gep instruction.How can I do
it?
My English is not so good, sorry
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
