java: rewrite conflict detection

- favour unary predicates over binary ones
(the natural "conflicting access" is binary)
- switch to a dual solution to trade recursion through forall for simple existentials.

Co-authored-by: Anders Schack-Mulligen <aschackmull@github.com>
This commit is contained in:
yoff
2025-10-17 01:39:29 +02:00
parent 5109babd92
commit 61a3e9630f
11 changed files with 296 additions and 323 deletions

View File

@@ -12,25 +12,25 @@ public class C {
public void m() {
this.y = 0; // $ Alert
this.y += 1;
this.y = this.y - 1;
this.y += 1; // $ Alert
this.y = this.y - 1; // $ Alert
}
public void n4() {
this.y = 0;
this.y += 1;
this.y = this.y - 1;
this.y = 0; // $ Alert
this.y += 1; // $ Alert
this.y = this.y - 1; // $ Alert
}
public void setY(int y) {
this.y = y;
this.y = y; // $ Alert
}
public void test() {
if (y == 0) {
if (y == 0) { // $ Alert
lock.lock();
}
y = 0;
y = 0; // $ Alert
lock.unlock();
}