On Mar 25, 2011, at 12:21 PM, Xiao Qu wrote:
> Another question I have is about declaring a single member of a structure as
> symbolic. For example (test.c),
>
> typedef struct
> {
> int a;
> int b;
> }ss;
>
> int main()
> {
> ss c;
> klee_make_symbolic(&c.a, sizeof(c.a), "input1");
> c.b = klee_int("input2");
> // ... ...
> }
>
> after building with llvm-gcc, I run "klee test.o"
> --- error occurs for "c.a" like KLEE: ERROR: wrong size given to
> klee_make_symbolic[_name], but there was nothing wrong with "c.b". How could
> this happen? Can I declare single structure members as symbolic or I must
> declare the whole object as symbolic?
At the moment, KLEE only supports making entire memory objects symbolic. KLEE
recognizes that the size you passed to klee_make_symbolic() doesn't match the
size of the whole object and returns that error. If you need this behavior, I
recommend making a separate variable of the correct size symbolic and then
assigning it to the struct member.
-David
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20110325/c6bd6b00/attachment.html
