[klee-dev] Help needed on generating bitcode

Tue Jul 16 09:12:35 BST 2013

Hello,

> Yes the problem is in the 4th step. Configure is working, but in the end says --disable-nls not identified. Without that flag configure shows no errors.
According to the gcc specification 
--disable-nlsThe --enable-nls option enables Native Language Support (NLS),
which lets GCC output diagnostics in languages other than American
English.  Native Language Support is enabled by default if not doing a
canadian cross build.  The --disable-nls option disables NLS.

     Have no suggestions.

> Python is installed on the system. 
Fine.

> I believe we need to change the klee-gcc to something else (maybe llvm-gcc, i tried that but this also showed errors)

I don't think so. 
Did klee were installed with no errors? 
The obj-llvm uses klee for its installation, maybe problem is somewhere previous?

Have no suggestions otherwise.

Urmas Repinski

On Tue, Jul 16, 2013 at 3:55 AM, Urmas Repinski <urrimus at hotmail.com> wrote:

Hello, Anas.

The problem is in tutorial 4 step 2 right?

coreutils-6.11$ mkdir obj-llvm
coreutils-6.11$ cd obj-llvm
obj-llvm$ ../configure --disable-nls CFLAGS="-g"
... verify that configure worked ...
obj-llvm$ make CC=/full/path/to/klee/scripts/klee-gcc
obj-llvm$ make -C src arch hostname CC=/full/path/to/klee/scripts/klee-gcc
... verify that make worked ...

Did configure finished with no error?

Possibly you cannot install obj-llvm, because its configure finished with error....

According to error some python2.7 folder does not exists.
Try to install python2.7 then too if configure passed successfully.

Urmas Repinski

From: anas.faruqui at gmail.com

Date: Tue, 16 Jul 2013 03:43:45 -0400
Subject: Re: [klee-dev] Help needed on generating bitcode
To: urrimus at hotmail.com
CC: klee-dev at imperial.ac.uk

Hi Urmas,
Thanks for the reply.
I am actually referring to the 4th tutorial, the core-utils one.
I want to run klee on gzip 1.6. This is an open source soft, and one needs to do configure and make to generate the binaries, similar to what is done in core-utils tutorial, but the same commands are not working. Maybe you can throw some light on that.

Thanks-Anas

On Tue, Jul 16, 2013 at 3:39 AM, Urmas Repinski <urrimus at hotmail.com> wrote:

Hello, Anas.

The thing is that according to the tutorial you should use llvm-gcc to compile KLEE instrumented program.
http://klee.llvm.org/Tutorial-1.html

llvm-gcc --emit-llvm -c -g get_sign.c

I had installed llvm-gcc using terminal command line, "apt-get install llvm-gcc" and this worked fine for me.

If default version does not compile instrumented code, then you can try to download and install previous version, http://llvm.org/releases/download.html .

Urmas Repinski.

From: anas.faruqui at gmail.com
Date: Mon, 15 Jul 2013 19:04:32 -0400
To: klee-dev at imperial.ac.uk

Subject: [klee-dev] Help needed on generating bitcode

Hi Everyone,
I am new to this area. I am trying to run KLEE on gzip 1.6, but am unable to gerate the llvm bitcode.

 I used the  make CC=/full/path/to/klee/scripts/klee-gcc  command as described in the tutorial. But it is giving this error

make  all-recursivemake[1]: Entering directory `/home/john/gzip-1.6/obj-llvm'

Making all in libmake[2]: Entering directory `/home/john/gzip-1.6/obj-llvm/lib'make  all-am

make[3]: Entering directory `/home/john/gzip-1.6/obj-llvm/lib'make[3]: Leaving directory `/home/john/gzip-1.6/obj-llvm/lib'

make[2]: Leaving directory `/home/john/gzip-1.6/obj-llvm/lib'Making all in docmake[2]: Entering directory `/home/john/gzip-1.6/obj-llvm/doc'

make[2]: Nothing to be done for `all'.make[2]: Leaving directory `/home/john/gzip-1.6/obj-llvm/doc'

Making all in .make[2]: Entering directory `/home/john/gzip-1.6/obj-llvm'  CCLD     gzip

Traceback (most recent call last):  File "/home/john/work/klee/scripts/klee-gcc", line 34, in <module>

    main()  File "/home/john/work/klee/scripts/klee-gcc", line 30, in main    os.execvp("llvm-ld", ["llvm-ld", "--disable-opt"] + linkArgs)

  File "/usr/lib/python2.7/os.py", line 344, in execvp    _execvpe(file, args)  File "/usr/lib/python2.7/os.py", line 380, in _execvpe

    func(fullname, *argrest)OSError: [Errno 2] No such file or directorymake[2]: *** [gzip] Error 1

make[2]: Leaving directory `/home/john/gzip-1.6/obj-llvm'make[1]: *** [all-recursive] Error 1

make[1]: Leaving directory `/home/john/gzip-1.6/obj-llvm'make: *** [all] Error 2

Any suggestion on how i can generate the bit code
Thanks-Anas

_______________________________________________
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