Greetings, While testing Klee with some programs that make use of library calls such as fork(), wait(), and kill() (including the one attached), I noticed that the Klee interpreter executes them concretely, thus forking new interpreter processes, and also sending real signals to other processes. In particular the "kill(getpid(), 9);" statement in the program under test immediately terminates Klee, when first reached by an execution state.
This behavior seems in contradiction with the fact that Klee has stub definitions for these calls in its POSIX runtime environment, in runtime/POSIX/illegal.c. But the assembly.ll file shows these definitions as external, instead of containing the code for them as defined by Klee, thus forcing Klee to execute concrete calls on them. Is this intended behavior, or there is an issue with the LLVM linking stage when preparing the final module? Thanks, Stefan Bucur -------------- next part -------------- A non-text attachment was scrubbed... Name: testfrk.c Type: text/x-csrc Size: 466 bytes Desc: not available Url : http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20100404/1931a66d/attachment.bin
