goblint / analyzer

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

Fix witness `enter` sync map when caller state changes #1462

Closed sim642 closed 1 month ago

sim642 commented 1 month ago

Closes #1453. Turns out this had nothing to do with abortUnless emitting an event from combine_env (where the crash came from).

Rather, it was caused by abortUnless's enter returning false as the caller state (for combine_env), rather than ctx.local. The witness lifter assumed it to always be ctx.local. abortUnless might be the only analysis which uses this aspect of enter, which is why this never occurred before.

TODO