[klee-dev] Give symbolic value When (read from out of bound pointer)

徐永健 xuyongjiande at gmail.com
Wed Dec 24 05:59:52 GMT 2014


Hi,

When klee got "memory error: out of bound pointer", it terminate the state.
But in some case, what I want is: giving symbolic value when the code
reading from 'out of bound pointer'.
Can I make this idea work?

I tried this:

```
std::string name = "test";
MemoryObject *mo = memory->allocate(bytes, false, true, unbound->pc->inst);
Array array = new Array(name, bytes);
ObjectState *os = bindObjectInState(*unbound, mo, false, array);
executeMakeSymbolic(*unbound, mo, name);
ref<Expr> result = os->read(0, type);
bindLocal(target, *unbound, result);
```
But klee got 'segment fault' in 'bindLocal()'. Can anyone tell me the
reason or give me a better solution?

Thanks.
-------------- next part --------------
HTML attachment scrubbed and removed


More information about the klee-dev mailing list