Even more to the point, printf doesn't actually return "blablah 42\n" at all -- it writes it to stdout as a side-effect. So you can't even say "simulate execution and see the result" without knowing that a particular small piece of inline assembly deep inside the libc stdio that was called near the end of printf() execution happens to trigger kernel magic. It's really just not feasible to do this type of optimization in the general case. And it's just impossible in this specific case, as mentioned by khim.