<html dir="ltr">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<style id="owaParaStyle" type="text/css">P {margin-top:0;margin-bottom:0;}</style>
</head>
<body ocsi="0" fpstyle="1">
<div style="direction: ltr;font-family: Tahoma;color: #000000;font-size: 10pt;"><br>
Hi,<br>
<br>
I am going to look into the ArrayBoundChecker. Currently it doesn't handle symbolic constraints on indexing with '>' or '<' properly.
<br>
<br>
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.<br>
<br>
cheers!,<br>
<br>
Per<br>
<br>
<br>
<br>
The ArrayBound check doesn't find this error:<font face="Courier New"><br>
<br>
void writeOutOfBoundsGEConstraint(int x) {<br>
int a[10];<br>
if (x >= 10)<br>
a[x] = 5; // ← 1. write access GE does not generate error<br>
}<br>
<br>
<font face="Tahoma">It does however find the read access with '>', but only using ArrayBound, _not_ ArrayBoundV2.</font><br>
<br>
int readOutOfBoundsGEConstraint(int x) {<br>
int a[10];<br>
int g=5;<br>
if (x >= 10)<br>
g = a[x]; // ← 2. read access GE generate error on V0<br>
return g;<br>
}<br>
</font><br>
<font face="Courier New"><font face="Courier New">out-of-bounds_2.c:13:9: warning: Access out-of-bound array element (buffer overflow)<br>
g = a[x]; // ← 2. read access GE generate error on V0<br>
^~~~<br>
<br>
</font><font face="Tahoma">The rest below are found in both ArrayBound and ArrayBoundV2:</font><br>
<br>
void writeOutOfBoundsEQ(int x) {<br>
int a[10];<br>
if (x == 10)<br>
a[x] = 0; // ← 3. write access EQ generate error on V0 and V2<br>
}<br>
<br>
out-of-bounds_2.c:20:11: warning: Access out-of-bound array element (buffer overflow)<br>
a[x] = 0; // ← 3. write access EQ generate error on V0 and V2<br>
~~~~ ^<br>
<br>
int readOutOfBoundsEQ(int x) {<br>
int a[10];<br>
int g=5;<br>
if (x == 10)<br>
g = a[x]; // ← 4. read access EQ generate error on V0 and V2<br>
return g;<br>
}<br>
<br>
out-of-bounds_2.c:26:9: warning: Access out-of-bound array element (buffer overflow)<br>
g = a[x]; // ← 4. read access EQ generate error on V0 and V2<br>
^~~~<br>
<br>
</font><br>
<br>
<br>
<br>
<br>
<div><br>
<div style="font-size:13px; font-family:Tahoma">
<p class="MsoNormal"><span style="font-size:8pt; font-family:'Arial','sans-serif'; color:gray" lang="EN-US">.......................................................................................................................</span><span style="font-size:8pt; font-family:'Arial','sans-serif'; color:black" lang="EN-US"><br>
Per Viberg </span><span style="font-size:8pt; font-family:'Arial','sans-serif'; color:gray" lang="EN-US">Senior Engineer</span><span style="font-size:8.5pt; font-family:'Arial','sans-serif'; color:gray" lang="EN-US"><br>
Evidente ES East</span><span style="font-size:8pt; font-family:'Arial','sans-serif'; color:gray" lang="EN-US"> AB Warfvinges väg 34 SE-112 51 Stockholm Sweden
</span><span style="font-size:10pt; font-family:'Tahoma','sans-serif'; color:black" lang="EN-US"></span></p>
<p class="MsoNormal"><span style="font-size:8pt; font-family:'Arial','sans-serif'; color:gray" lang="EN-GB">Phone: +46 (0)8 402 79 00<br>
Mobile: +46 (0)70 912 42 52<br>
E-mail: <a href="mailto:Per.Viberg@evidente.se" target="_blank"><font color="#0000ff">Per.Viberg@evidente.se</font></a>
</span><span style="font-size:8pt; font-family:'Arial','sans-serif'; color:black" lang="EN-GB"><br>
<br>
<a href="http://www.evidente.se" target="_blank"><font color="#0000ff">www.evidente.se</font></a></span></p>
<p class="MsoNormal"><span style="font-size:6pt; font-family:'Arial','sans-serif'" lang="EN-GB">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.</span></p>
</div>
</div>
</div>
</body>
</html>