[klee-dev] Space program in KLEE Using concolic method

[Andrew Santosa]

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
Regards,Andrew



| 
| 
|  | 
Symbolic Environment · KLEE


 |

 |

 |




 

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

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 KLEE.

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 at imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
  
-------------- next part --------------
HTML attachment scrubbed and removed