[klee-dev] Some Question about Klee

[Tomasz Kuchta]

Adding the list ..

On 12/04/13 16:59, Tomasz Kuchta wrote:
> Hi Paul,
> 
> Regarding your first question - try compiling with --emit-llvm option.
> If compiler returns errors about c99 mode, you may want to try -std=c99
> option as well.
> 
> Best Regards,
> 
> Tomek
> 
> On 12/04/13 16:11, 明白了 wrote:
>> Sorry to interrupt you, but I really need some help in the problems I
>> come across:
>> The first question is the following error:
>> bx at ubuntu:~/work/klee/examples/sort$
>> <mailto:bx at ubuntu:~/work/klee/examples/sort$> llvm-gcc -I ../../include
>> -c -g sort.c
>> bx at ubuntu:~/work/klee/examples/sort$
>> <mailto:bx at ubuntu:~/work/klee/examples/sort$> klee sort.o
>> KLEE: ERROR: error loading program 'sort.o': Invalid bitcode signature
>> bx at ubuntu:~/work/klee/examples/sort$
>> <mailto:bx at ubuntu:~/work/klee/examples/sort$> ls
>> sort.c sort.c~ sort.o
>> bx at ubuntu:~/work/klee/examples/sort$
>> <mailto:bx at ubuntu:~/work/klee/examples/sort$> klee
>> --only-output-states-covering-new sort.o
>> KLEE: ERROR: error loading program 'sort.o': Invalid bitcode signature
>> When compiling the file sort.c in the example category of klee, it
>> generates file sort.o. But when the file sort.o isn’t used, it will
>> report this error, saying it’s an invalid bitcode signature. I can’t
>> figure out what’s wrong with this.
>>  
>> The second question is :
>> We installs the system 12.04 version of klee according to the installing
>> steps that you publish on the web, but it reports the error above when
>> compiling, saying it is a “unrecognized option ‘--emit-llvm’”. Why was
>> it so? I need some help in this.
>>
>> And the last question is that, how to test the whole project together
>> instead of testing the files one by one? What’s more, the examples you
>> give are all involved with a function klee_make_symblic which is used in
>> the main function. This function has a parameter that is the variable of
>> the function to be tested. Do you just provide testing examples that are
>> only involved the paths which are related to this variable?
>> Thank you for taking time to read these. I am hoping for your reply.
>> Thank you very much.
>> Yours sincerely,
>> Paul
>>
>>
>>
>> _______________________________________________
>> klee-dev mailing list
>> klee-dev at imperial.ac.uk
>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>>
> 
>