Java: Accept guards test results.

This commit is contained in:
Anders Schack-Mulligen
2025-09-05 09:33:10 +02:00
parent 60d07cf30d
commit e8f1ec68db
2 changed files with 8 additions and 6 deletions

View File

@@ -26,7 +26,7 @@ public class Guards {
}
int sz = a != null ? a.length : 0;
for (int i = 0; i < sz; i++) {
chk(); // $ guarded='a != null:true' guarded='i < sz:true' guarded='sz:not 0' guarded='...?...:...:not 0' guarded='a.length:not 0' guarded='a:not null'
chk(); // $ guarded='a != null:true' guarded='i < sz:true' guarded='sz:Lower bound 1' guarded='...?...:...:Lower bound 1' guarded='a.length:Lower bound 1' guarded='a:not null'
int e = a[i];
if (e > 2) break;
}
@@ -136,11 +136,11 @@ public class Guards {
found = true;
}
if (found) {
chk(); // $ guarded=found:true guarded='i < a.length:true'
chk(); // $ guarded=found:true guarded='i < a.length:true' guarded='a.length:Lower bound 1'
}
}
if (found) {
chk(); // $ guarded=found:true guarded='i < a.length:false'
chk(); // $ guarded=found:true guarded='i < a.length:false' guarded='i:Lower bound 0'
}
}

View File

@@ -8,12 +8,12 @@
| Guards.java:25:7:25:11 | chk(...) | b:false |
| Guards.java:25:7:25:11 | chk(...) | g(1):true |
| Guards.java:25:7:25:11 | chk(...) | g(2):false |
| Guards.java:29:7:29:11 | chk(...) | '...?...:...:not 0' |
| Guards.java:29:7:29:11 | chk(...) | '...?...:...:Lower bound 1' |
| Guards.java:29:7:29:11 | chk(...) | 'a != null:true' |
| Guards.java:29:7:29:11 | chk(...) | 'a.length:not 0' |
| Guards.java:29:7:29:11 | chk(...) | 'a.length:Lower bound 1' |
| Guards.java:29:7:29:11 | chk(...) | 'a:not null' |
| Guards.java:29:7:29:11 | chk(...) | 'i < sz:true' |
| Guards.java:29:7:29:11 | chk(...) | 'sz:not 0' |
| Guards.java:29:7:29:11 | chk(...) | 'sz:Lower bound 1' |
| Guards.java:39:9:39:13 | chk(...) | 's:bar' |
| Guards.java:39:9:39:13 | chk(...) | 's:match "bar"' |
| Guards.java:42:9:42:13 | chk(...) | 's:foo' |
@@ -85,9 +85,11 @@
| Guards.java:127:7:127:11 | chk(...) | 'o != null:false' |
| Guards.java:127:7:127:11 | chk(...) | 'o:null' |
| Guards.java:127:7:127:11 | chk(...) | g(1):false |
| Guards.java:139:9:139:13 | chk(...) | 'a.length:Lower bound 1' |
| Guards.java:139:9:139:13 | chk(...) | 'i < a.length:true' |
| Guards.java:139:9:139:13 | chk(...) | found:true |
| Guards.java:143:7:143:11 | chk(...) | 'i < a.length:false' |
| Guards.java:143:7:143:11 | chk(...) | 'i:Lower bound 0' |
| Guards.java:143:7:143:11 | chk(...) | found:true |
| Guards.java:173:7:173:11 | chk(...) | 's:not null' |
| Guards.java:173:7:173:11 | chk(...) | testNotNull1(...):true |