<!---
name: Symbolic execution
route: /docs/cpp/advanced/symbolic-execution
parent: Documentation
menu: Advanced
description: Describe how UTBotCpp symbolic execution
--->

UTBot runs KLEE by fork() + exec() method and controls symbolic execution via waitpid(). UTBot uses Z3 version 4.8.7 as
SMT-solver for KLEE. Symbolic execution of each function under test issues a separate KLEE run, which symbolically
executes the function wrapper generated by UTBot. UTBot gives KLEE a configurable amount of time to symbolically execute
given bitcode, and, when it ends, sends KLEE a SIGINT signal, which is correctly handled by KLEE in many cases — the
engine saves explored paths and finishes the execution. However, there are scenarios where KLEE does not handle SIGINTs
correctly due to missing handlers in some parts of its code; so UTBot waits a specified amount of time and then sends
stronger signals: SIGSTOP, and, eventually, SIGKILL. UTBot KLEE configuration. UTBot runs KLEE with the following
parameters:

```shell
klee --entry-point=klee_entry__max
--libc=klee --posix-runtime --fp-runtime
--only-output-states-covering-new 
--allocate-determ --external-calls=all 
--timer-interval=1s --bcov-check-interval=5s
--disable-verify --output-dir=klee-out-dir
bitcode.bc --sym-stdin 64
```

Let us explain every KLEE command line option passed by UTBot in detail:

* KLEE is given a bitcode representation of a project target, which may contain many functions, so KLEE understands
  where to begin symbolic execution by an entry-point option. To improve symbolic execution possibilities, KLEE needs to
  be supplied with standard C library, i.e. libc, compiled into LLVM IR. There is a choice one can make between using
  KLEE libc — a small set of libc functions shipped with KLEE itself,
  or [klee-uclibc](https://github.com/klee/klee-uclibc), a more complete package, which can be linked with KLEE and used
  during symbolic execution. Again (as with POSIX runtime), this KLEE libc or klee-uclibc library can be treated as
  stubs that used by KLEE instead of real libc. UTBot uses KLEE libc. Despite that a wider set of functions is
  implemented in klee-uclibc, using it forces KLEE to analyse additional several thousands of LLVM instructions prior to
  analysing actual code of UTBot wrapper, consequently, slowing down UTBot test generation. It is understood that
  coverage may be lost using –libc=klee instead of –libc=uclibc, so it is planned to make the libc selection
  configurable;
* UTBot uses KLEE POSIX runtime and self-developed floatingpoint runtime library to allow symbolic execution of programs
  operating with file descriptors and floating-point values;
* –only-output-states-covering-new option is used to not generate tests executing the same path in user functions;
* UTBot allows all external calls to discard minimal number of branches. External call is a possibility of KLEE to
  execute a function not implemented in LLVM IR. For that, function arguments are concretized, which potentially leads
  to a coverage loss, but other options of handling external function calls, like killing an execution branch, are even
  worse in terms of achieving maximal coverage;
* timer-interval and self-invented bcov-check-interval are used to stop symbolic execution of branches not promising to
  increase coverage;
* UTBot allows using 64 bytes of symbolic stdin;
* UTBot uses –disable-verify as its linking procedure (Section 3.3) passes only correct bitcode to KLEE.