[klee-dev] How to handle 32bit bc file with 64bit klee

Nowack, Martin m.nowack at imperial.ac.uk
Tue Dec 15 14:35:31 GMT 2020


Hi,
There are a couple of missing features.
Can you open an issue https://github.com/klee/klee/issues ? we can continue the discussion there.

Best,
Martin

On 15. Dec 2020, at 13:41, JingXiaoni <jingxiaoni at icloud.com<mailto:jingxiaoni at icloud.com>> wrote:


Hi all,
l have some problems
on using klee,need your help .Thanks in advance
My test target is 32bit app.Now I compile llvm and klee in x86_64, then add -m32 option on compile target object.
For example:
for bc file
clang++ -m32 sample.cpp -c -o sample.bc
for app
clang++ -m32 sample.cpp -o sample -lkleeRuntest
Now I have 2 issues
1. bc file compile is success.But when I use klee to generate test cases.There is a error info"LLVM ERROR:64-bit code requested on a subtarget that doesn't support it". I would like to make klee can handle 32bit bc.Then add option in CMakeList.txt with add_complie_option(--target=i386-pc-linux-gun).remake makefile and make,make has a warning that "cc1 plus:warning:command line option '-ftarget=i386-pc-linux-gun'is valid for Java but not for c++".Add Klee can’t work for 32 bit bc,too.
So my question is how to add compile options in cmake or make file to make 64bit Klee can support 32bit bc file?
2.When I compile 32 bit app with Klee lib(libKleeRuntest),It shows can’t find this lib but when I compile 64bit app,there is no problem.Does it mean I need to compile a 32bit Klee to use it or is there some other way to set it up and it will work?
Thanks for your help.


_______________________________________________
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


More information about the klee-dev mailing list