Hi,

On Tue, 23 May 2023 16:38:25 +0900
Nguyễn Gia Phong <[email protected]> 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

_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Reply via email to