Hi, It turned out to be a problem with my running script, and not one with Klee. The --posix-runtime parameter was not passed to Klee, and therefore that code didn't end up being linked into the final module. Sorry for all the noise...
Cheers, Stefan On Mon, Apr 5, 2010 at 12:00 AM, Stefan Bucur <stefan.bucur at epfl.ch> wrote: > 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 >
