[klee-dev] KLEE behaviour with function call to uclibc

[Dan Liew]

Hi,

On 28 May 2017 at 00:55, Shehbaz Jaffer <shehbaz.jaffer at 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.