[klee-dev] Use of -sym-stdin/stdout

[Frank Busse]

Hi,


On Tue, 23 May 2023 16:38:25 +0900
Nguyễn Gia Phong <mcsinyx at disroot.org> wrote:

> Do you recall the reason for that default,
> i.e. what are the potential drawbacks of enabling
> symbolic printf in KLEE's µClibc?

printf has to transform its parameters into strings. This is heavily
branching code (even worse when the format string is symbolic). Have a
look e.g. at musl's implementation:

https://git.musl-libc.org/cgit/musl/tree/src/stdio/vfprintf.c


Kind regards,

Frank