There is an unsaved comment in progress. You will lose your changes if you continue. Are you sure you want to reopen the work item?
missing check on claim destruction in atomics
The soundness of treating atomic actions as atomic depends on the objects in the closed object list remaining closed for the duration of the atomic. By historical accident, VCC implements this with a coarser check that no objects are unwrapped within an
atomic. However, this check is not performed on claim destruction (which is just syntactic sugar for an unwrapping along with some updates), creating an unsoundness. A check should be added that destroyed claims are not mentioned in the closed object list.