At least on sv-benchmarks this has no measurable impact OLS regression on CPU time gives $$y = 0.98x + 0.01$$ without outliars. It's also the case that sv-benchmarks uses library functions a lot less than real-world programs would.

Still, we need to do this to be sound, there's no way around it. If this turns out to negatively impact some realistic benchmarks, we might want to optimize something, but that's a separate matter.

To comment on a few of these:

• There are some library functions that explicitly do not evaluate their arguments (or at least not with the usual semantics (such as the sizeof operator which iirc we map to a library function). Do we need to account for those?

SizeOfE is actually a constructor in Cil.exp, so that shouldn't be the problem.

• This adds such evaluation to the base analysis. Do other analyses also need it?

Only if they produce warnings from domains during expression evaluation, but I don't know if that is the case anywhere else.
The other obvious candidate is relation analysis, but it doesn't even do structural evaluation.
The access/race analysis already covers this, e.g. 04-mutex/20-stdfun_rc.

• Is eval_rv always the right thing to do? Do arguments to library functions not sometimes act as lvals?

To act as an lval, the argument needs to be AddrOf lval, not just lval. And anyway we have to evaluate things in lvals as well, e.g. pointer arithmetic under * or indexing expressions.

I can add more tests if you'd like, but we can put whatever we want in the printf arguments, and it will cause the bug to happen again. I put some more examples because I wasn't sure about the cause of the issue.

I would also be interested to see the effect of this on a larger set of benchmarks, say the concrat suite...

Using the setup now at goblint/bench#69, the total number of evals changes 2300528 → 2305052, which is an increase of 4524, i.e. 0.2%.