@@ -8,7 +8,7 @@ int test1(struct List* p) {
88 int count = 0 ;
99 for (; p; p = p->next ) {
1010 count = count+1 ;
11- range (count); // $ range="==Phi: p: Store: count+1"
11+ range (count); // $ range="==Phi: p | Store: count+1"
1212 }
1313 range (count);
1414 return count;
@@ -18,7 +18,7 @@ int test2(struct List* p) {
1818 int count = 0 ;
1919 for (; p; p = p->next ) {
2020 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"
2222 }
2323 range (count); // $ range=>=-9 range=<=9
2424 return count;
@@ -29,7 +29,7 @@ int test3(struct List* p) {
2929 for (; p; p = p->next ) {
3030 range (count++); // $ range=>=-9 range=<=9
3131 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"
3333 }
3434 range (count); // $ range=>=-9 range=<=9
3535 return count;
@@ -93,12 +93,12 @@ int test8(int x, int y) {
9393 if (-1000 < y && y < 10 ) {
9494 range (y); // $ range=<=9 range=>=-999
9595 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"
9898 return x;
9999 }
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
102102 }
103103 range (x);
104104 range (y);
@@ -128,11 +128,11 @@ int test10(int x, int y) {
128128 range (y); // $ range=>=8
129129 if (x < y) {
130130 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"
132132 return 0 ;
133133 }
134134 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
136136 return x;
137137 }
138138 range (y); // $ range=<=7
@@ -541,7 +541,7 @@ int test16(int x) {
541541 while (i < 3 ) {
542542 range (i); // $ range=<=2 range=>=0
543543 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"
545545 }
546546 range (d);
547547 d = i;
@@ -640,14 +640,14 @@ unsigned int test_comma01(unsigned int x) {
640640 unsigned int y1;
641641 unsigned int y2;
642642 y1 = (++y, y);
643- range (y1); // $ range=<=101 range="==Phi: ... ? ... : ...: Store: ... ? ... : ...+1"
643+ range (y1); // $ range=<=101 range="==Phi: ... ? ... : ... | Store: ... ? ... : ...+1"
644644 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"
646646 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"
648648 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"
651651 return y1 + y2;
652652}
653653
@@ -672,7 +672,7 @@ void test17() {
672672 range (i); // $ range===50
673673
674674 i = 20 + (j -= 10 );
675- range (i); // $ range="==Store: ... += ...: Store: ... = ...+10" range===60
675+ range (i); // $ range="==Store: ... += ... | Store: ... = ...+10" range===60
676676}
677677
678678// Tests for unsigned multiplication.
0 commit comments