Hi Daniel,
I have tried it on a simple program containing klee_int but it fails. Did
I miss anything?
Specifically, I changed klee_make_symbolic(&c, sizeof(c), "input") in
"islower.c" to int c = klee_int("input"). Then I run "gcc -I ../include
../Release/lib/libkleeRuntest.so islower.c" as I did to the original
"islower.c" (this one was successful as described in tutorial one):
--- the build error shows as: undefined reference to "klee_int"
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?
Thanks!
Xiao
Daniel Dunbar <daniel at zuster.org>
Sent by: daniel.dunbar at gmail.com
10/01/2010 11:45 AM
To
Xiao Qu/USABB/ABB at ABB
cc
klee-dev at keeda.stanford.edu, klee-dev-bounces at keeda.stanford.edu, LI LEI
<leimli.hit at gmail.com>, nobled <nobled at dreamwidth.org>
Subject
Re: [klee-dev] replay with library
Yes, the replay library is supposed to contain versions of all the
KLEE intrinsics that will work during replay. Most of them are just
simple wrappers around klee_make_symbolic.
- Daniel
On Wed, Sep 29, 2010 at 7:44 PM, <xiao.qu at us.abb.com> wrote:
>
> Hello everyone,
>
> In tutorial one, it says "KLEE provides a convenient replay library,
which
> simply replaces the call to klee_make_symbolic with a call to a function
> that assigns to our input the value stored in the .ktest file". Does
this
> also work if the program contains other klee methods such as klee_int ?
>
> Thanks,
> Xiao
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20110325/8dbbd727/attachment.html
