@@ -8,7 +8,7 @@ int test1(struct List* p) {
8
8
int count = 0 ;
9
9
for (; p; p = p->next ) {
10
10
count = count+1 ;
11
- range (count); // $ range="==Phi: p: Store: count+1"
11
+ range (count); // $ range="==Phi: p | Store: count+1"
12
12
}
13
13
range (count);
14
14
return count;
@@ -18,7 +18,7 @@ int test2(struct List* p) {
18
18
int count = 0 ;
19
19
for (; p; p = p->next ) {
20
20
count = (count+1 ) % 10 ;
21
- range (count); // $ range=<=9 range=>=-9 range="<=Phi: p: Store: count+1"
21
+ range (count); // $ range=<=9 range=>=-9 range="<=Phi: p | Store: count+1"
22
22
}
23
23
range (count); // $ range=>=-9 range=<=9
24
24
return count;
@@ -29,7 +29,7 @@ int test3(struct List* p) {
29
29
for (; p; p = p->next ) {
30
30
range (count++); // $ range=>=-9 range=<=9
31
31
count = count % 10 ;
32
- range (count); // $ range=<=9 range=>=-9 range="<=Store: ... +++0" range="<=Phi: p: Store: count+1"
32
+ range (count); // $ range=<=9 range=>=-9 range="<=Store: ... +++0" range="<=Phi: p | Store: count+1"
33
33
}
34
34
range (count); // $ range=>=-9 range=<=9
35
35
return count;
@@ -93,12 +93,12 @@ int test8(int x, int y) {
93
93
if (-1000 < y && y < 10 ) {
94
94
range (y); // $ range=<=9 range=>=-999
95
95
if (x < y-2 ) {
96
- range (x); // $ range=<=6 range="<=InitializeParameter: y: Store: y-3"
97
- range (y); // $ range=<=9 range=>=-999 range=">=InitializeParameter: x: Store: x+3"
96
+ range (x); // $ range=<=6 range="<=InitializeParameter: y | Store: y-3"
97
+ range (y); // $ range=<=9 range=>=-999 range=">=InitializeParameter: x | Store: x+3"
98
98
return x;
99
99
}
100
- range (x); // $ range=>=-1001 range=">=InitializeParameter: y: Store: y-2"
101
- range (y); // $ range=<=9 range="<=InitializeParameter: x: Store: x+2" range=>=-999
100
+ range (x); // $ range=>=-1001 range=">=InitializeParameter: y | Store: y-2"
101
+ range (y); // $ range=<=9 range="<=InitializeParameter: x | Store: x+2" range=>=-999
102
102
}
103
103
range (x);
104
104
range (y);
@@ -128,11 +128,11 @@ int test10(int x, int y) {
128
128
range (y); // $ range=>=8
129
129
if (x < y) {
130
130
range (x); // $ range="<=InitializeParameter: y-1"
131
- range (y); // $ range=>=8 range=">=InitializeParameter: x: Store: x+1"
131
+ range (y); // $ range=>=8 range=">=InitializeParameter: x | Store: x+1"
132
132
return 0 ;
133
133
}
134
134
range (x); // $ range=>=8 range=">=InitializeParameter: y+0"
135
- range (y); // $ range="<=InitializeParameter: x: Store: x+0" range=>=8
135
+ range (y); // $ range="<=InitializeParameter: x | Store: x+0" range=>=8
136
136
return x;
137
137
}
138
138
range (y); // $ range=<=7
@@ -541,7 +541,7 @@ int test16(int x) {
541
541
while (i < 3 ) {
542
542
range (i); // $ range=<=2 range=>=0
543
543
i++;
544
- range (i); // $ range=<=3 range=>=1 range="==Phi: i: Store: ... = ...+1"
544
+ range (i); // $ range=<=3 range=>=1 range="==Phi: i | Store: ... = ...+1"
545
545
}
546
546
range (d);
547
547
d = i;
@@ -640,14 +640,14 @@ unsigned int test_comma01(unsigned int x) {
640
640
unsigned int y1;
641
641
unsigned int y2;
642
642
y1 = (++y, y);
643
- range (y1); // $ range=<=101 range="==Phi: ... ? ... : ...: Store: ... ? ... : ...+1"
643
+ range (y1); // $ range=<=101 range="==Phi: ... ? ... : ... | Store: ... ? ... : ...+1"
644
644
y2 = (y++,
645
- range (y), // $ range=<=102 range="==Store: ++ ...: Store: ... = ...+1" range="==Phi: ... ? ... : ...: Store: ... ? ... : ...+2"
645
+ range (y), // $ range=<=102 range="==Store: ++ ... | Store: ... = ...+1" range="==Phi: ... ? ... : ... | Store: ... ? ... : ...+2"
646
646
y += 3 ,
647
- range (y), // $ range=<=105 range="==Store: ++ ...: Store: ... = ...+4" range="==Store: ... +++3" range="==Phi: ... ? ... : ...: Store: ... ? ... : ...+5"
647
+ range (y), // $ range=<=105 range="==Store: ++ ... | Store: ... = ...+4" range="==Store: ... +++3" range="==Phi: ... ? ... : ... | Store: ... ? ... : ...+5"
648
648
y);
649
- range (y2); // $ range=<=105 range="==Store: ++ ...: Store: ... = ...+4" range="==Store: ... +++3" Unexpected result: range="==Phi: ... ? ... : ...: Store: ... ? ... : ...+5"
650
- range (y1 + y2); // $ range=<=206 range="<=Phi: ... ? ... : ...: Store: ... ? ... : ...+106" MISSING: range=">=++ ...:... = ...+5" range=">=... +++4" range=">=... += ...:... = ...+1" range=">=... ? ... : ...+6"
649
+ range (y2); // $ range=<=105 range="==Store: ++ ... | Store: ... = ...+4" range="==Store: ... +++3" Unexpected result: range="==Phi: ... ? ... : ... | Store: ... ? ... : ...+5"
650
+ range (y1 + y2); // $ range=<=206 range="<=Phi: ... ? ... : ... | Store: ... ? ... : ...+106" MISSING: range=">=++ ...:... = ...+5" range=">=... +++4" range=">=... += ...:... = ...+1" range=">=... ? ... : ...+6"
651
651
return y1 + y2;
652
652
}
653
653
@@ -672,7 +672,7 @@ void test17() {
672
672
range (i); // $ range===50
673
673
674
674
i = 20 + (j -= 10 );
675
- range (i); // $ range="==Store: ... += ...: Store: ... = ...+10" range===60
675
+ range (i); // $ range="==Store: ... += ... | Store: ... = ...+10" range===60
676
676
}
677
677
678
678
// Tests for unsigned multiplication.
0 commit comments