[klee-dev] How to compile without using "-c" when building KLEE tutorial?

[Nowack, Martin]

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 <lebron716 at outlook.com<mailto:lebron716 at outlook.com>> wrote:

This email from lebron716 at outlook.com<mailto:lebron716 at outlook.com> 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
klee-dev at imperial.ac.uk<mailto:klee-dev at imperial.ac.uk>
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

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