[klee-dev] [Question] What is the correct/efficient way to implement a separate execution without affecting the normal execution in KLEE?

2024-03-26 Thread TU Haoxin
Dear KLEE developers, May I ask a question about implementing a separate execution in KLEE? My initial idea is to separate ("simulate") running a state and evaluate whether this state is worthy of exploring in the future further. I will use the attached figure to explain what I want to do

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

2024-01-31 Thread TU Haoxin
38#other-trials Thanks, Haoxin From: Nguyễn Gia Phong Sent: Wednesday, January 31, 2024 13:34 To: TU Haoxin; klee-dev@imperial.ac.uk<mailto:klee-dev@imperial.ac.uk> Subject: Re: [klee-dev] Different behavior of KLEE when testing `dircolors` with "--optimize=true/false" optio

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

2024-01-30 Thread TU Haoxin
: Nguyễn Gia Phong Sent: Wednesday, January 31, 2024 13:34 To: TU Haoxin; klee-dev@imperial.ac.uk Subject: Re: [klee-dev] Different behavior of KLEE when testing `dircolors` with "--optimize=true/false" option On 2024-01-31 at 05:07+00:00, TU Haoxin wrote: > The behavior is that KLEE

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

2024-01-30 Thread 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

[klee-dev] Different behavior when invoking the "error" function with the argument buffer from heap or stack

2024-01-24 Thread TU Haoxin
Dear KLEE developers, Hope you are all doing well, and hope this is the right place to raise questions about KLEE. I have a question regarding the modeling of the function `error` function in `klee-uclibc` when I used KLEE. Since I couldn't find similar cases either in the GitHub issue or the