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

[Daniel Schemmel]

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
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev