Hi, On 28 May 2017 at 00:55, Shehbaz Jaffer <shehbaz.jaf...@mail.utoronto.ca> wrote: > Hi Dan, > > > Thank you for your reply. However, I am struggling with how function not > defined in the programs bitcode (like getopt_long function) gets emulated by > KLEE. Please allow me to explain the steps and where I am facing issues in > more detail:
getopt_long is part of the C library. In KLEE's case the definition can be found in klee-uclibc. If you don't link in klee-uclibc (i.e. with `-libc=uclibc`) then the `getopt_long()` won't get linked into the final LLVM IR that gets executed. Side note KLEE has the ability to call external functions (i.e. those not defined in LLVM IR) but JIT'ing calls to that function but doing this requires that KLEE concretize all arguments to the function. When running KLEE take a look at the `assembly.ll` file in the klee output directory (e.g. `klee-last`). That file shows the LLVM IR that KLEE actually executes. This IR contains the result of KLEE linking in whatever libraries it decided to link in (e.g. klee-uclibc) and the result of then applying any transformation passes to the IR. _______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
