klee
klee copied to clipboard
klee
Solver timeout inconsistency
Right now the --max-solver-time option accepts a double argument. However, that argument is truncated to an integer before calling the solver because the timer is enforced by means of alarm(unsigned seconds).
This might cause confusion and also makes the minimum solver timeout 1 second.
Confusion can be avoided by making the --max-solver-time take an integer or we can be more flexible by using setitimer.
Good catch. We should definitely implement one of these solutions. I guess the setitimer is indeed more flexible. Do you want to write a patch implementing one of them?
@251 I believe this very old issue was solved by the new time API you contributed a couple of years back. This being said, I still see a few alarm calls in the codebase. Is this issue still present after your changes?
@ccadar Yes, upstream still uses alarm and is limited to seconds. MoKlee has a sigtimedwait implementation though - shall I create a PR?
@251 thanks. Would sigtimedwait work on macOS and FreeBSD? Maybe you can use sigwait instead?
@ccadar sigtimedwait is part of POSIX and sigwait is implemented on top of sigtimedwait in Linux acc. to the man page. Should work for all of them.