[klee-dev] direct symbolic execution

[Yijia Gu]

Hi All,

Does KLEE now support the "directed symbolic execution" - efficiently
finding program executions that reach user-specified target line
(http://www.cs.umd.edu/~jfoster/papers/sas11.pdf) ?

For example,

int test(){
  if(success){
     while(...){}
  }else{
     fail();
  }
}

I want KLEE to skip the while loops in the success branch and explore the
fail branch directly.

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