|
To enable the POSIX support, the former implementation instrumented the
main function and inserted a call to `klee_init_env` at the beginning.
This has multiple disadvantages:
* debugging information was not correctly propagated leaving the call to
`klee_init_env` without debug information
* the main function always required `int arg, char**` as part of the
function definition of `main`
Based on the new linking infrastructure, we can now add an additional
wrapper `__klee_posix_wraper(int, char**)` that gets always called when
POSIX support is enabled. It executes `klee_init_env` and after that
calls the `main` function.
Enabling POSIX support only requires the renaming of the user provided
`main` into `__klee_posix_wrapped_main` in addition to linking.
|
