Hi Norlina,
Yes, generally it is possible for KLEE to generate string inputs, including a 
program written in a particular language.For the space program that you are 
testing, I guess that you would need to provide a symbolic file as an input 
program.KLEE will then replace the content of the file with concrete contents 
in the generated .ktest files.

Please have a look on how to use symbolic files in this tutorial: Symbolic 
Environment · KLEE

|  | 
Symbolic Environment · KLEE





    On Tuesday, 13 February 2018, 6:19:06 pm GMT+8, Norlina Pasaribu 
<norli...@xlfutureleaders.com> wrote:  

I am so really thankful having chance to get KLEE contact. My name is Norlina 
Pasaribu from Institut Teknologi Del, Indonesia. Now, I am in my last year of 
my bachelor and getting a thesis abouttesting program. If you don't mind, let 
me to tell you a little about my project.

We are really proud of you for buliding a KLEE tools for testing. I have Space 
program being the object for the testing. Space is C program contains 9000 line 
codes and I get from http://sir.unl.edu/.  
I found on some paper, that concolic testing is possible to implemented using 

My plan is I would like to generate test-case for Space program using concolic 
testing method in KLEE. Space input is not numerical but Array Defenition 
Language (ADL). 

My question is, is that possible KLEE for generating test-case and for 
non-numerical input ?

We really hope we be able to discuss more about it with you. If you dont mind, 
let us to get your respond. 
Thank you very much for attention.
Best regards,
Norlina Pasaribu_______________________________________________
klee-dev mailing list
klee-dev mailing list

Reply via email to