@@ -1039,7 +1039,7 @@ void test_guard_after_use(int pos, int size, int offset) {
1039
1039
if (offset == 1 ) {
1040
1040
return ;
1041
1041
}
1042
- range (pos + 1 ); // $ overflow=+ range="==InitializeParameter: pos+1"
1042
+ range (pos + 1 ); // $ overflow=+ range="==InitializeParameter: pos+1" MISSING: range="<=InitializeParameter: size-1"
1043
1043
}
1044
1044
1045
1045
int cond ();
@@ -1060,8 +1060,8 @@ void alloc_in_loop(int origLen) {
1060
1060
}
1061
1061
len = len * 2 ; // $ overflow=-
1062
1062
}
1063
- // We want that index <= len
1064
- range (index);
1063
+ // We want that index < len
1064
+ range (index); // $ MISSING: range="<=InitializeParameter: len-1"
1065
1065
index++;
1066
1066
}
1067
1067
}
@@ -1079,7 +1079,7 @@ void mask_at_start(int len) {
1079
1079
for (int index = leftOver; index < len; index+=64 ) {
1080
1080
range (index); // $ range="<=InitializeParameter: len-1"
1081
1081
// This should be in bounds
1082
- range (index + 16 ); // $ range="<=InitializeParameter: len+15" range="==Phi: index+16"
1082
+ range (index + 16 ); // $ range="<=InitializeParameter: len+15" range="==Phi: index+16" MISSING: range="<=InitializeParameter: len-1"
1083
1083
}
1084
1084
}
1085
1085
@@ -1096,7 +1096,7 @@ void mod_at_start(int len) {
1096
1096
// Do something with leftOver
1097
1097
for (int index = leftOver; index < len; index+=64 ) {
1098
1098
range (index); // $ range="<=InitializeParameter: len-1"
1099
- // This should be in bounds
1100
- range (index + 16 ); // $ range="<=InitializeParameter: len+15" range="==Phi: index+16"
1099
+ // This should be in bounds
1100
+ range (index + 16 ); // $ range="<=InitializeParameter: len+15" range="==Phi: index+16" MISSING: range="<=InitializeParameter: len-49"
1101
1101
}
1102
1102
}
0 commit comments