You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
A separate T is to be introduced that conceptually ranges over the entire environment. I gave it a shot today, but turns out it is a major rewrite that I don't have time for before wrapping up my thesis.
Among other things, it and also entails carefully thinking about where variable values are only forgotten as opposed to removed from the environment.
Creating this separate issue for the principled fix allows merging #1354 which is not the grand unified fix but a step in the right direction (and away from a setup which we know to be unsound) which also allows for experiments in a setting that is not unsound.
The text was updated successfully, but these errors were encountered:
Is this not just a workaround for the actual bug? Seems like escapes should also contribute to mutex_inits. BasePriv.PerMutexPrivBase and BasePriv.PerMutexMeetTIDPriv side-effect escapes to mutex_inits at least.
As discussed here
https://github.com/goblint/analyzer/pull/1354/files/05bd808ad40aea8555f53f1d235f257d26d67988#r1498877891
and in the GobCon.
A separate T is to be introduced that conceptually ranges over the entire environment. I gave it a shot today, but turns out it is a major rewrite that I don't have time for before wrapping up my thesis.
Among other things, it and also entails carefully thinking about where variable values are only forgotten as opposed to removed from the environment.
Creating this separate issue for the principled fix allows merging #1354 which is not the grand unified fix but a step in the right direction (and away from a setup which we know to be unsound) which also allows for experiments in a setting that is not unsound.
The text was updated successfully, but these errors were encountered: