about summary refs log tree commit diff homepage
path: root/runtime/POSIX/fd.h
diff options
context:
space:
mode:
authorMartin Nowack <m.nowack@imperial.ac.uk>2018-07-22 23:12:49 +0100
committerCristian Cadar <c.cadar@imperial.ac.uk>2018-09-10 15:24:17 +0100
commit3d373d8b5c101e0798ea8a5e8015aa03537d02d8 (patch)
treedbf0f42bd7707b4c2d2505be803c770c70f6dceb /runtime/POSIX/fd.h
parent0f1b68e093dfe0357adf400ea7b4746f09fb4cba (diff)
downloadklee-3d373d8b5c101e0798ea8a5e8015aa03537d02d8.tar.gz
POSIX: Add invocation of klee_init_env into wrapper before calling main
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.
Diffstat (limited to 'runtime/POSIX/fd.h')
0 files changed, 0 insertions, 0 deletions