[klee-dev] make reading from file symbolic

[Urmas Repinski]

Hello.

I have some program, named schedule.c, that i want symbolically evaluate using klee, to generate inputs.

Inside the program i have some fscanf(stdin, "%d", &command) comes, and with "%f" argument also.

I want to make this command variable symbolic, no difference to generate symbolic input file for it, ot to make it as usual variable and to generate inputs.

When i compile the code with llvm-gcc, then compilation is success and .o file is generated.

But when i execute .o file using klee - 

klee  schedule.o

I get :

KLEE: WARNING: undefined reference to function: 
__isoc99_fscanf
KLEE: WARNING: undefined reference to variable: stdin
KLEE: WARNING ONCE: calling external: 
__isoc99_fscanf(140528011303360, 51367536, 51252160)

and no inputs is generated, execution stops.

Obviously necessary to replace the reading from stdin by  --sym-files parameters, but if i add

klee  schedule.o --sym-files 0 20

0 - means that no addition files needed, stdin only, and 20 some arbitrary number, size of data.

When i hit Ctrl+C then 5 inputs are generated, but not in this variables what i want.

Please suggest any possible parameters combination, i think to avoid warnings necessary to remove fscanf from original code, but in this case klee will not know what variables to make symbolic.....

Urmas Repinski

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