Java: Fix bad magic in SynchSetUnsynchGet.

This commit is contained in:
Anders Schack-Mulligen
2021-11-08 11:42:20 +01:00
parent e9b114630a
commit 92fb7f555c

View File

@@ -35,6 +35,7 @@ predicate isSynchronizedByBlock(Method m) {
* In this case, even if `set` is synchronized and `get` is not, `get` will never see stale
* values for the field, so synchronization is optional.
*/
pragma[nomagic]
predicate bothAccessVolatileField(Method set, Method get) {
exists(Field f | f.isVolatile() |
f = get.(GetterMethod).getField() and