[klee-dev] symbolic variable appears in the offset of a pointer or an array

[im]

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&gt;, I append two constraints that x &gt;=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
-------------- next part --------------
HTML attachment scrubbed and removed