[klee-dev] How can I get KLEE to generate constraints from within function calls

Dan Liew dan at su-root.co.uk
Sat Mar 19 12:41:04 GMT 2016


On 18 March 2016 at 15:00, Sumit Kumar <sumit686215 at gmail.com> wrote:
> Hi,
>
> My test program is this: I declare 'x' as symbolic and then pass the address
> / value of x as argument to function foo like foo(x) or foo(&x). Inside the
> function foo no variables have been explicitly made symbolic.

Based on your description it sounds like the address of ``x`` is not
symbolic. The contents of memory that ``x`` points to is.

> Now when I run
> KLEE I do not see any constraints generated from foo. How can I get KLEE to
> generate constraints from within function calls. I am using KLEE with
> llvm2.9.

Your question is far too vague. If you write a precise question you
are more likely to get a useful answer.




More information about the klee-dev mailing list