Skip to content

Commit 0d7ebd5

Browse files
committed
Fixed a problem where the rw_set range's upper bound not set correctly
1 parent fae6a48 commit 0d7ebd5

File tree

3 files changed

+37
-1
lines changed

3 files changed

+37
-1
lines changed
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
int main()
2+
{
3+
int a[10];
4+
a[2] = 2;
5+
a[1] = 1;
6+
int out = a[2];
7+
return out;
8+
}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
CORE
2+
main.c
3+
--dependence-graph --show
4+
activate-multi-line-match
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
// Assignment has a data dependency on the assignment of a[2]
8+
\/\/ ([0-9]+).*\n.*a\[\(signed long int\)2\] = 2;(.*\n)*Data dependencies: (\1)\n(.*\n){2,3}.*out = *
9+
--
10+
// Assignment has no data dependency on the assignment of a[1]
11+
\/\/ ([0-9]+).*\n.*a\[\(signed long int\)1\] = 1;(.*\n)*Data dependencies: (\1)\n(.*\n){2,3}.*out = *
12+
^warning: ignoring
13+
--
14+
15+
The two regex above matches output portions like shown below (with <N> being a
16+
location number). The intention is to make sure the rw_set recognize the range
17+
of the assignment to an array index correctly.
18+
19+
// <N> file main.c line 4 function main
20+
a[(signed long int)2] = 2;
21+
...
22+
23+
**** 4 file main.c line 6 function main
24+
Data dependencies: <N>
25+
26+
// 4 file main.c line 6 function main
27+
out = a[(signed long int)2];
28+

src/analyses/goto_rw.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -542,7 +542,7 @@ void rw_range_sett::get_objects_rec(
542542
{
543543
range_spect range_end=size==-1 ? -1 : range_start+size;
544544
if(size!=-1 && full_size!=-1)
545-
range_end=std::max(range_end, full_size);
545+
range_end=std::min(range_end, full_size);
546546

547547
add(mode, identifier, range_start, range_end);
548548
}

0 commit comments

Comments
 (0)