[klee-dev] Asking for Help about Klee3.4 on docker

[Andrea Mattavelli]

Hi Jiarui,
in the first case you are running extract-bc on the wrong object: extract-bc must be run on the executable (base64) and not on the object file.
In the second case the problem is that you are running configure with wllvm without specifying LLVM_COMPILER=clang (configure: error: C compiler cannot create executables). Try to look into config.log to confirm the problem.

You can find some more explanations on the wllvm page: https://github.com/travitch/whole-program-llvm <https://github.com/travitch/whole-program-llvm>

Best,
Andrea

> On 16 Mar 2016, at 10:09, Jiarui Wang <jrwwang at ucdavis.edu> wrote:
> 
> Hi, 
> 
> I followed   Tutorial on How to Use KLEE to Test GNU Coreutils http://klee.github.io/tutorials/testing-coreutils/ <http://klee.github.io/tutorials/testing-coreutils/>  .
> 
> In the step 2, I got all the *.o files by using whole-program-llvm. But there is no *.bc files.
> 
> So I used 
> 
> klee at 3cc1aa045534:~/test/coreutils-6.11/obj-llvm/src$ /home/klee/test/whole-program-llvm-master/extract-bc base64.o
> 
> to get *.bc files. But I got the error 
> 
> klee at 3cc1aa045534:~/test/coreutils-6.11/obj-llvm/src$ /home/klee/test/whole-program-llvm-master/extract-bc base64.o
> DEBUG::popenwrapper.Popen() at popenwrapper.py:13 ::WLLVM Executing:
> ['file', '/home/klee/test/coreutils-6.11/obj-llvm/src/base64.o']
> in: /home/klee/test/coreutils-6.11/obj-llvm/src
> DEBUG::extract-bc.process_file_unix() at extract-bc:341 ::Detected file type is ELF_OBJECT
> INFO::extract-bc.process_file_unix() at extract-bc:348 ::Generating LLVM Bitcode module
> DEBUG::popenwrapper.Popen() at popenwrapper.py:13 ::WLLVM Executing:
> ['objdump', '-h', '-w', 'base64.o']
> in: /home/klee/test/coreutils-6.11/obj-llvm/src
> Traceback (most recent call last):
>   File "/home/klee/test/whole-program-llvm-master/extract-bc", line 380, in <module>
>     sys.exit(main(sys.argv))
>   File "/home/klee/test/whole-program-llvm-master/extract-bc", line 327, in main
>     process_file_unix(inputFile, outputFile, llvmLinker, llvmArchiver)
>   File "/home/klee/test/whole-program-llvm-master/extract-bc", line 349, in process_file_unix
>     return handleExecutable(inputFile, outputFile, extractor, llvmLinker)
>   File "/home/klee/test/whole-program-llvm-master/extract-bc", line 139, in handleExecutable
>     fileNames = extractor(inputFile)
>   File "/home/klee/test/whole-program-llvm-master/extract-bc", line 129, in extract_section_linux
>     (sectionSize, sectionOffset) = getSectionSizeAndOffset(elfSectionName, inputFile)
>   File "/home/klee/test/whole-program-llvm-master/extract-bc", line 79, in getSectionSizeAndOffset
>     filename)
> Exception: Could not find ".llvm_bc" ELF section in "base64.o"
> 
> Just like this email https://www.mail-archive.com/klee-dev@imperial.ac.uk/msg01926.html <https://www.mail-archive.com/klee-dev@imperial.ac.uk/msg01926.html>  and it does not work for both base64 and base64.o
> 
> Then I tried 
> ```
> export WLLVM_OUTPUT=DEBUG
> export CC=wllvm
> export CXX=wllvm++
>  ../configure --disable-nls CFLAGS="-g"
> make
> ```
> when I run ../configure --disable-nls CFLAGS="-g”  there was an error
> klee at 3cc1aa045534:~/test/coreutils-6.11/obj-llvm$ ../configure --disable-nls CFLAGS="-g"
> checking build system type... x86_64-unknown-linux-gnu
> checking host system type... x86_64-unknown-linux-gnu
> configure: autobuild project... GNU coreutils
> configure: autobuild revision... 6.11
> configure: autobuild hostname... 3cc1aa045534
> configure: autobuild timestamp... 20160316-095126
> checking for a BSD-compatible install... /usr/bin/install -c
> checking whether build environment is sane... yes
> checking for a thread-safe mkdir -p... /bin/mkdir -p
> checking for gawk... no
> checking for mawk... mawk
> checking whether make sets $(MAKE)... yes
> checking for style of include used by make... GNU
> checking for gcc... wllvm
> checking for C compiler default output file name... 
> configure: error: C compiler cannot create executables
> See `config.log' for more details.
> Hope you can help me asap.
> Thank you very much
> Jiarui Wang
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

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