Skip to content

Commit 6d872c1

Browse files
author
Matthieu Lemerre
committed
shorter C
1 parent 4537c02 commit 6d872c1

File tree

1 file changed

+2
-6
lines changed

1 file changed

+2
-6
lines changed

papers/2025-pldi-relational-abstractions-labeled-uf.md

Lines changed: 2 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -100,12 +100,8 @@ a sound static analyzer based on abstract interpretation, and in [Colibri2](http
100100
Codex already performs constraint propagation using relations between the values computed by the program. However, the new domain can find new relations; in particular, an important source of improvement comes from relating
101101
simultaneously incremented loop counters. For instance, consider the following C snippet:
102102
```c
103-
int i = 0;
104-
int j = 4;
105-
while(i < 10) {
106-
i += 1;
107-
j += 3;
108-
}
103+
int i = 0, j = 4;
104+
while(i < 10) { i += 1; j += 3; }
109105
```
110106
Without labeled union-find, Codex learns that at the end of the loop, $$\mathtt{i} = 10$$,
111107
$$\mathtt{j} \in [4:+\infty]$$ and $$\mathtt{j} \equiv 1 \mathop{\mathtt{mod}} 3$$. However,

0 commit comments

Comments
 (0)