@@ -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
21
+ range (count); // $ range=<=9 range=<=count:p+1
22
22
}
23
23
range (count); // $ 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
31
31
count = count % 10 ;
32
- range (count); // $ range=<=9
32
+ range (count); // $ range=<=9 range="<=... +++0" range=<=count:p+1
33
33
}
34
34
range (count); // $ range=<=9
35
35
return count;
@@ -40,13 +40,13 @@ int test4() {
40
40
int total = 0 ;
41
41
for (i = 0 ; i < 2 ; i = i+1 ) {
42
42
range (i); // $ range=<=1 range=>=0
43
- range (total);
43
+ range (total); // $ range=>=0
44
44
total += i;
45
- range (total);
45
+ range (total); // $ range=>=0 range=>=i+0
46
46
}
47
- range (total);
47
+ range (total); // $ range=>=0
48
48
range (i); // $ range===2
49
- range (total + i); // $ range=>=i+1
49
+ range (total + i); // $ range=>=i+1 range=>=2 range=>=i+0
50
50
return total + i;
51
51
}
52
52
@@ -55,13 +55,13 @@ int test5() {
55
55
int total = 0 ;
56
56
for (i = 0 ; i < 2 ; i++) {
57
57
range (i); // $ range=<=1 range=>=0
58
- range (total);
58
+ range (total); // $ range=>=0
59
59
total += i;
60
- range (total);
60
+ range (total); // $ range=>=0 range=>=i+0
61
61
}
62
- range (total);
62
+ range (total); // $ range=>=0
63
63
range (i); // $ range===2
64
- range (total + i); // $ range=>=i+1
64
+ range (total + i); // $ range=>=i+1 range=>=2 range=>=i+0
65
65
return total + i;
66
66
}
67
67
@@ -70,9 +70,9 @@ int test6() {
70
70
int total = 0 ;
71
71
for (i = 0 ; i+2 < 4 ; i = i+1 ) {
72
72
range (i); // $ range=<=1 range=>=0
73
- range (total);
73
+ range (total); // $ range=>=0
74
74
total += i;
75
- range (total);
75
+ range (total); // $ range=>=0 range=>=i+0
76
76
}
77
77
return total + i;
78
78
}
@@ -149,7 +149,7 @@ int test11(char *p) {
149
149
range (*p);
150
150
}
151
151
if (c == ' :' ) {
152
- range (c);
152
+ range (c); // $ range===58
153
153
c = *p;
154
154
range (*p);
155
155
if (c != ' \0 ' ) {
@@ -310,15 +310,15 @@ int test_mult01(int a, int b) {
310
310
int r = a*b; // 0 .. 253
311
311
range (r);
312
312
total += r;
313
- range (total); // $ range=>=0 range=>=3+0
313
+ range (total); // $ range=>=0 range=>=3+0 range=">=... * ...+0"
314
314
}
315
315
if (3 <= a && a <= 11 && -13 <= b && b <= 23 ) {
316
316
range (a); // $ range=<=11 range=>=3
317
317
range (b); // $ range=<=23 range=>=-13
318
318
int r = a*b; // -143 .. 253
319
319
range (r);
320
320
total += r;
321
- range (total);
321
+ range (total); // $ range=">=... * ...+0"
322
322
}
323
323
if (3 <= a && a <= 11 && -13 <= b && b <= 0 ) {
324
324
range (a); // $ range=<=11 range=>=3
@@ -358,15 +358,15 @@ int test_mult02(int a, int b) {
358
358
int r = a*b; // 0 .. 253
359
359
range (r);
360
360
total += r;
361
- range (total); // $ range=>=0 range=>=0+0
361
+ range (total); // $ range=>=0 range=>=0+0 range=">=... * ...+0"
362
362
}
363
363
if (0 <= a && a <= 11 && -13 <= b && b <= 23 ) {
364
364
range (a); // $ range=<=11 range=>=0
365
365
range (b); // $ range=<=23 range=>=-13
366
366
int r = a*b; // -143 .. 253
367
367
range (r);
368
368
total += r;
369
- range (total);
369
+ range (total); // $ range=">=... * ...+0"
370
370
}
371
371
if (0 <= a && a <= 11 && -13 <= b && b <= 0 ) {
372
372
range (a); // $ range=<=11 range=>=0
@@ -453,15 +453,15 @@ int test_mult04(int a, int b) {
453
453
int r = a*b; // -391 .. 0
454
454
range (r);
455
455
total += r;
456
- range (total); // $ range="<=- ...+0" range=<=0
456
+ range (total); // $ range="<=- ...+0" range=<=0 range="<=... * ...+0"
457
457
}
458
458
if (-17 <= a && a <= 0 && -13 <= b && b <= 23 ) {
459
459
range (a); // $ range=<=0 range=>=-17
460
460
range (b); // $ range=<=23 range=>=-13
461
461
int r = a*b; // -391 .. 221
462
462
range (r);
463
463
total += r;
464
- range (total);
464
+ range (total); // $ range="<=... * ...+0"
465
465
}
466
466
if (-17 <= a && a <= 0 && -13 <= b && b <= 0 ) {
467
467
range (a); // $ range=<=0 range=>=-17
@@ -501,15 +501,15 @@ int test_mult05(int a, int b) {
501
501
int r = a*b; // -391 .. 0
502
502
range (r);
503
503
total += r;
504
- range (total); // $ range="<=- ...+0" range=<=0
504
+ range (total); // $ range="<=- ...+0" range=<=0 range="<=... * ...+0"
505
505
}
506
506
if (-17 <= a && a <= -2 && -13 <= b && b <= 23 ) {
507
507
range (a); // $ range=<=-2 range=>=-17
508
508
range (b); // $ range=<=23 range=>=-13
509
509
int r = a*b; // -391 .. 221
510
510
range (r);
511
511
total += r;
512
- range (total);
512
+ range (total); // $ range="<=... * ...+0"
513
513
}
514
514
if (-17 <= a && a <= -2 && -13 <= b && b <= 0 ) {
515
515
range (a); // $ range=<=-2 range=>=-17
@@ -628,7 +628,7 @@ unsigned int test_ternary02(unsigned int x) {
628
628
(range (x), 5 ); // $ range=>=300
629
629
range (y5); // y6 >= 0
630
630
}
631
- range (y1 + y2 + y3 + y4 + y5); // $ range=">=... = ...:... ? ... : ...+0 " range=">=call to range+0 "
631
+ range (y1 + y2 + y3 + y4 + y5); // $ range=">=... = ...:... ? ... : ...+1 " range=">=call to range+1 "
632
632
return y1 + y2 + y3 + y4 + y5;
633
633
}
634
634
@@ -693,15 +693,15 @@ int test_unsigned_mult01(unsigned int a, unsigned b) {
693
693
int r = a*b; // 0 .. 253
694
694
range (r);
695
695
total += r;
696
- range (total); // $ range=">=(unsigned int)...+0" range=>=0
696
+ range (total); // $ range=">=(unsigned int)...+0" range=>=0 range=>=(int)...+0
697
697
}
698
698
if (3 <= a && a <= 11 && 13 <= b && b <= 23 ) {
699
699
range (a); // $ range=<=11 range=>=3
700
700
range (b); // $ range=<=23 range=>=13
701
701
int r = a*b; // 39 .. 253
702
702
range (r);
703
703
total += r;
704
- range (total); // $ range=">=(unsigned int)...+1" range=>=1
704
+ range (total); // $ range=">=(unsigned int)...+1" range=>=1 range=>=(int)...+0
705
705
}
706
706
range (total); // $ range=">=(unsigned int)...+0" range=>=0
707
707
return total;
@@ -722,14 +722,14 @@ int test_unsigned_mult02(unsigned b) {
722
722
int r = 11 *b; // 0 .. 253
723
723
range (r);
724
724
total += r;
725
- range (total); // $ range=">=(unsigned int)...+0" range=>=0
725
+ range (total); // $ range=">=(unsigned int)...+0" range=>=0 range=>=(int)...+0
726
726
}
727
727
if (13 <= b && b <= 23 ) {
728
728
range (b); // $ range=<=23 range=>=13
729
729
int r = 11 *b; // 143 .. 253
730
730
range (r);
731
731
total += r;
732
- range (total); // $ range=">=(unsigned int)...+1" range=>=1
732
+ range (total); // $ range=">=(unsigned int)...+1" range=>=1 range=>=(int)...+0
733
733
}
734
734
range (total); // $ range=">=(unsigned int)...+0" range=>=0
735
735
return total;
@@ -856,18 +856,18 @@ int notequal_type_endpoint(unsigned n) {
856
856
857
857
void notequal_refinement (short n) {
858
858
if (n < 0 ) {
859
- range (n);
859
+ range (n); // $ range=<=-1
860
860
return ;
861
861
}
862
862
863
863
if (n == 0 ) {
864
864
range (n); // 0 .. 0
865
865
} else {
866
- range (n); // 1 ..
866
+ range (n); // $ range=>=1
867
867
}
868
868
869
869
if (n) {
870
- range (n); // 1 ..
870
+ range (n); // $ range=>=1
871
871
} else {
872
872
range (n); // 0 .. 0
873
873
}
@@ -883,25 +883,29 @@ void notequal_refinement(short n) {
883
883
void notequal_variations (short n, float f) {
884
884
if (n != 0 ) {
885
885
if (n >= 0 ) {
886
- range (n); // 1 .. [BUG: we can't handle `!=` coming first]
886
+ range (n); // $ range=>=1
887
887
}
888
888
}
889
889
890
890
if (n >= 5 ) {
891
891
if (2 * n - 10 == 0 ) { // Same as `n == 10/2` (modulo overflow)
892
- range (n);
892
+ range (n); // $ range=>=5 MISSING: range===5
893
893
return ;
894
894
}
895
- range (n); // 6 ..
895
+ range (n); // $ range=>=5 MISSING: range=>=6
896
896
}
897
897
898
898
if (n != -32768 && n != -32767 ) {
899
899
range (n); // -32766 ..
900
900
}
901
901
902
902
if (n >= 0 ) {
903
- n ? (range (n), n) : (range (n), n); // ? 1.. : 0..0
904
- !n ? (range (n), n) : (range (n), n); // ? 0..0 : 1..
903
+ n ?
904
+ (range (n), n) // $ range=>=1
905
+ : (range (n), n); // $ MISSING: range===0
906
+ !n ?
907
+ (range (n), n) // $ MISSING: range===0
908
+ : (range (n), n); // $ range=>=1
905
909
}
906
910
}
907
911
@@ -917,7 +921,7 @@ void two_bounds_from_one_test(short ss, unsigned short us) {
917
921
}
918
922
919
923
if (ss < 0x8001 ) { // Lower bound removed in `getDefLowerBounds`
920
- range (ss); // - 32768 .. 32767
924
+ range (ss); // $ range=<= 32768 MISSING: range=>=-32768
921
925
}
922
926
923
927
if ((short )us >= 0 ) {
@@ -942,7 +946,7 @@ void widen_recursive_expr() {
942
946
for (s = 0 ; s < 10 ; s++) {
943
947
range (s); // $ range=<=9 range=>=0
944
948
int result = s + s;
945
- range (result); // 0 .. 18
949
+ range (result); // $ range=>=0 range=>=s+0 // 0 .. 18
946
950
}
947
951
}
948
952
0 commit comments