Privatizations unsound when threadflag analysis deactivated

Open sim642 opened this issue 3 years ago • 0 comments

In #859 one of the autotune unsoundness cases was caused by autotune deactivating the threadflag analysis. A minimized TODO test is added here: https://github.com/goblint/analyzer/pull/859/commits/505b66949e488060daf82413a399b328d05b4ebc.

The problem is, when threadflag is deactivated, EnterMultithreaded event is never emitted and thus privatizations don't correctly publish initial values, in that particular case to MUTEX_INITS. I'm not sure which privatizations (both base and apron) are affected, possibly all non-trivial ones.

Oct 19 '22 07:10 sim642