[klee-dev] Different behavior of KLEE when testing `dircolors` with "--optimize=true/false" option

[TU Haoxin]

Dear KLEE developers,


I found an interesting behavior of KLEE while using a variant tool of KLEE (https://github.com/haoxintu/SymLoc) to test the dircolors​ package in GNU Coreutils. The behavior is that KLEE fails to fork at a branch that should be forked with the option --optimize option enabled (i.e., --optimize=true). While the --optimize option is disabled (i.e., --optimize=false), the branch can be successfully forked as usual.


Please check more details at https://gist.github.com/haoxintu/183dda2923965d1e33f64ad59c7f5338. (I recorded here mainly because the markdown format makes it easy to present some code examples).

Could you please look at this case and check if this is a potential issue in KLEE's optimization (LLVM's optimization probably)? Please also let me know if I can provide anything further.

Thank you very much for your time and help!


Best regards,

Haoxin



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