Hi Xuan,
I’m sorry for the very late reply.
The problem you are describing is the following:
The files you’re compiling, e.g. from `get_sign.c` do contain calls, which KLEE
handles internally (i.e. `klee_make_symbolic`):
```
...
int main() {
int a;
klee_make_symbolic(&a, sizeof(a), "a");
return get_sign(a);
}
```
Unfortunately, if you want to compile those applications to native code, you
have to provide an implementation for that, which you link against in the
linking step.
Depending on your use case the implementation might be either empty functions
or, for example in the re-run of tests, provide values that initialise the
variables appropriately.
As this problem is coming up quite often, I’ll open a PR for additional code
and documentation.
I hope that helps.
All the best,
Martin
On 21. Jan 2020, at 09:53, XIE Xuan
<[email protected]<mailto:[email protected]>> wrote:
This email from [email protected]<mailto:[email protected]> originates
from outside Imperial. Do not click on links and attachments unless you
recognise the sender. If you trust the sender, add them to your safe senders
list<https://spam.ic.ac.uk/SpamConsole/Senders.aspx> to disable email stamping
for this address.
Hi there,
I am now playing around KLEE and try to use clang to build bitcode file in the
first tutorial (http://klee.github.io/tutorials/testing-function/).
My command is: clang -I ../../include -g -emit-llvm -O0 -Xclang
-disable-O0-optnone get_sign.c
And it complain -emit-llvm cannot be used when linking.
I try: clang -I ../../include -g -O0 -Xclang -disable-O0-optnone get_sign.c
And it complains "undefined reference to 'klee_make_symbolic'" even I give all
the dependency(those .a file) of KLEE to wllvm. It should at least normally
compile even I am not using “-c -emit-llvm”. Does anyone know what’s the reason
for clang cannot find the dependency for KLEE library?
Thanks!
_______________________________________________
klee-dev mailing list
[email protected]<mailto:[email protected]>
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
