goblint / analyzer

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

Clear up meaning of `MayEscape` & Distinguish a local becoming reachable via globals from being reachable by other threads #1544

Open michael-schwarz opened 2 months ago

michael-schwarz commented 2 months ago

We make inconsistent assumptions about what "has escaped" is supposed to mean:

I came across this when considering #1542, where this distinction leads to a new global variable being created when reading to g#in that has not received any values as the value of the variable is still tracked locally.

sim642 commented 2 months ago

The description of the escape analysis should definitely at least be amended. I guess it would be possible to have two separate analyses and queries for the two different notions but that might be overkill. In the multi-threaded case they would probably have to amplify each other anyway.

Our notion of escaping would generalize anyway with #1491.