Hello,
if you wish to only execute a piece of code (such as `if (p[x] > 3) { /*
... */ }`) when a condition (such as `x >= 0 && x < sizeof(b) /
sizeof(*b)`) holds, you can use an if statement like this:
```
if (x >= 0 && x < sizeof(b) / sizeof(*b)) {
if (p[x] > 3){ /*...*/ }
if (b[x] > 3){ /*...*/ }
for (int i = 0;i < x;i++){ /* p[i] ... */ }
}
```
Best,
Daniel
On 2024-07-02 03:35, im wrote:
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
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
