[klee-dev] Problems with symbolic execution of 'rm' from the Coreutil

[Samaneh Navabpour]

Hi,

So I have a question regarding the symbolic execution of operation  
'rm' from the Coreutil.

Lets say I run:

klee --only-output-states-covering-new --optimize --libc=uclibc  
--posix-runtime ./rm.bc --sym-args 0 2 2

This instruction can hypothetically result in the execution of

rm -f /

In this case, by running the above Klee command I can destroy my file  
system. can I not??? or am I wrong?

Can someone please suggest a solution around this problem so I can  
symbolically execute 'rm' from the Coreutil.

Im facing the same problem when trying to use Klee to symbolically  
execute unlinking of files in libc.

Thank you
Samaneh

-- 
Samaneh Navabpour
Department of Electrical and Computer Engineering
University of Waterloo
200 University Avenue West
Waterloo, Ontario, Canada, N2L 3G1