Hi,
I am going to look into the ArrayBoundChecker. Currently it doesn't handle
symbolic constraints on indexing with '>' or '<' properly.
There are two implementation of the ArrayBoundChecker, and some errors are not
detected with the V2, (see below), so my main question is: Which of the
ArrayBoundV2 or ArrayBound is the one that should be improved on? Also, any
specific class/interfaces that should/shouldn't be used?. Any other useful
hints on where to fix this are also highly appreciated.
cheers!,
Per
The ArrayBound check doesn't find this error:
void writeOutOfBoundsGEConstraint(int x) {
int a[10];
if (x >= 10)
a[x] = 5; // ← 1. write access GE does not generate error
}
It does however find the read access with '>', but only using ArrayBound, _not_
ArrayBoundV2.
int readOutOfBoundsGEConstraint(int x) {
int a[10];
int g=5;
if (x >= 10)
g = a[x]; // ← 2. read access GE generate error on V0
return g;
}
out-of-bounds_2.c:13:9: warning: Access out-of-bound array element (buffer
overflow)
g = a[x]; // ← 2. read access GE generate error on V0
^~~~
The rest below are found in both ArrayBound and ArrayBoundV2:
void writeOutOfBoundsEQ(int x) {
int a[10];
if (x == 10)
a[x] = 0; // ← 3. write access EQ generate error on V0 and V2
}
out-of-bounds_2.c:20:11: warning: Access out-of-bound array element (buffer
overflow)
a[x] = 0; // ← 3. write access EQ generate error on V0 and V2
~~~~ ^
int readOutOfBoundsEQ(int x) {
int a[10];
int g=5;
if (x == 10)
g = a[x]; // ← 4. read access EQ generate error on V0 and V2
return g;
}
out-of-bounds_2.c:26:9: warning: Access out-of-bound array element (buffer
overflow)
g = a[x]; // ← 4. read access EQ generate error on V0 and V2
^~~~
.......................................................................................................................
Per Viberg Senior Engineer
Evidente ES East AB Warfvinges väg 34 SE-112 51 Stockholm Sweden
Phone: +46 (0)8 402 79 00
Mobile: +46 (0)70 912 42 52
E-mail: [email protected]<mailto:[email protected]>
www.evidente.se<http://www.evidente.se>
This e-mail, which might contain confidential information, is addressed to the
above stated person/company. If you are not the correct addressee, employee or
in any other way the person concerned, please notify the sender immediately. At
the same time, please delete this e-mail and destroy any prints. Thank You.
_______________________________________________
cfe-commits mailing list
[email protected]
http://lists.cs.uiuc.edu/mailman/listinfo/cfe-commits
