goblint / analyzer

Static analysis framework for C
https://goblint.in.tum.de
MIT License
172 stars 72 forks source link

Fix `ctx.split` and `ctx.spawn` in non-call transfer functions #1515

Closed sim642 closed 3 months ago

sim642 commented 3 months ago

Since OCaml evaluates arguments right-to-left, !r and !spawns are dereferenced before calling the transfer function, which will populate them (uselessly). By using let, evaluation order is enforced.

So far we've used ctx.split and ctx.spawn only on function call edges, specifically from special, which has a lot of other stuff around it, so it already had the evaluation order enforced by a let. That's why splitting worked at all (for those). But trying to split on other edges for more involved #1301 revealed paths not appearing due to this very subtle evaluation order issue.

It's not possible to test this with existing analyses, but it's also not possible to write sensible analysis for #1301 without this already being fixed.