From 0d7ebd55f95fe2e9a3547c500d3d4d899dc1eed0 Mon Sep 17 00:00:00 2001
From: zhixing-xu <zhixingx@princeton.edu>
Date: Mon, 6 Aug 2018 16:01:12 -0400
Subject: [PATCH 1/2] Fixed a problem where the rw_set range's upper bound not
 set correctly

---
 .../goto-analyzer/dependence-graph14/main.c   |  8 ++++++
 .../dependence-graph14/test.desc              | 28 +++++++++++++++++++
 src/analyses/goto_rw.cpp                      |  2 +-
 3 files changed, 37 insertions(+), 1 deletion(-)
 create mode 100644 regression/goto-analyzer/dependence-graph14/main.c
 create mode 100644 regression/goto-analyzer/dependence-graph14/test.desc

diff --git a/regression/goto-analyzer/dependence-graph14/main.c b/regression/goto-analyzer/dependence-graph14/main.c
new file mode 100644
index 00000000000..82d0a3aea19
--- /dev/null
+++ b/regression/goto-analyzer/dependence-graph14/main.c
@@ -0,0 +1,8 @@
+int main()
+{
+  int a[10];
+  a[2] = 2;
+  a[1] = 1;
+  int out = a[2];
+  return out;
+}
diff --git a/regression/goto-analyzer/dependence-graph14/test.desc b/regression/goto-analyzer/dependence-graph14/test.desc
new file mode 100644
index 00000000000..da93a09d59c
--- /dev/null
+++ b/regression/goto-analyzer/dependence-graph14/test.desc
@@ -0,0 +1,28 @@
+CORE
+main.c
+--dependence-graph --show
+activate-multi-line-match
+^EXIT=0$
+^SIGNAL=0$
+// Assignment has a data dependency on the assignment of a[2]
+\/\/ ([0-9]+).*\n.*a\[\(signed long int\)2\] = 2;(.*\n)*Data dependencies: (\1)\n(.*\n){2,3}.*out = *
+--
+// Assignment has no data dependency on the assignment of a[1]
+\/\/ ([0-9]+).*\n.*a\[\(signed long int\)1\] = 1;(.*\n)*Data dependencies: (\1)\n(.*\n){2,3}.*out = *
+^warning: ignoring
+--
+
+The two regex above matches output portions like shown below (with <N> being a
+location number). The intention is to make sure the rw_set recognize the range
+of the assignment to an array index correctly.
+
+        // <N> file main.c line 4 function main
+        a[(signed long int)2] = 2;
+        ...
+
+**** 4 file main.c line 6 function main
+Data dependencies: <N>
+
+        // 4 file main.c line 6 function main
+        out = a[(signed long int)2];
+
diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp
index 55236145ab8..61e7467669b 100644
--- a/src/analyses/goto_rw.cpp
+++ b/src/analyses/goto_rw.cpp
@@ -542,7 +542,7 @@ void rw_range_sett::get_objects_rec(
     {
       range_spect range_end=size==-1 ? -1 : range_start+size;
       if(size!=-1 && full_size!=-1)
-        range_end=std::max(range_end, full_size);
+        range_end=std::min(range_end, full_size);
 
       add(mode, identifier, range_start, range_end);
     }

From 2b403385099f694da55e11e5cc90e41763c8dd7e Mon Sep 17 00:00:00 2001
From: zhixing-xu <zhixingx@princeton.edu>
Date: Tue, 7 Aug 2018 09:44:52 -0400
Subject: [PATCH 2/2] Update test.desc

---
 regression/goto-analyzer/dependence-graph14/test.desc | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/regression/goto-analyzer/dependence-graph14/test.desc b/regression/goto-analyzer/dependence-graph14/test.desc
index da93a09d59c..bab0c027748 100644
--- a/regression/goto-analyzer/dependence-graph14/test.desc
+++ b/regression/goto-analyzer/dependence-graph14/test.desc
@@ -4,11 +4,9 @@ main.c
 activate-multi-line-match
 ^EXIT=0$
 ^SIGNAL=0$
-// Assignment has a data dependency on the assignment of a[2]
-\/\/ ([0-9]+).*\n.*a\[\(signed long int\)2\] = 2;(.*\n)*Data dependencies: (\1)\n(.*\n){2,3}.*out = *
+\/\/ ([0-9]+).*\n.*a\[\(signed long( long)? int\)2\] = 2;(.*\n)*Data dependencies: (\1)\n(.*\n){2,3}.*out = *
 --
-// Assignment has no data dependency on the assignment of a[1]
-\/\/ ([0-9]+).*\n.*a\[\(signed long int\)1\] = 1;(.*\n)*Data dependencies: (\1)\n(.*\n){2,3}.*out = *
+\/\/ ([0-9]+).*\n.*a\[\(signed long( long)? int\)1\] = 1;(.*\n)*Data dependencies: (\1)\n(.*\n){2,3}.*out = *
 ^warning: ignoring
 --