goblint / analyzer

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

Introduce sync reason `JoinCall` & Limit `sync` at function start nodes #1508

Closed michael-schwarz closed 2 weeks ago

michael-schwarz commented 3 weeks ago

Helps avoid "sync" calls for function start nodes when threadflag is context-sensitive. Previously, it was only avoided when the flag was path-sensitive (c.f. #1475).

This has some immediate termination advantages, and can potentially also boost precision.

TODO:

Closes #1507