From 1eb3f6f1e2c1d2d126fec1c939d58b2beacd3467 Mon Sep 17 00:00:00 2001
From: Jordy Ruiz <jruiz@ic.ac.uk>
Date: Fri, 3 Apr 2020 14:58:04 +0200
Subject: [PATCH 1/2] Add failing unit test for intersection of field-sensitive
 and field-insensitive fields

---
 test/Slicing/field-sensitivity-hetero.c | 32 +++++++++++++++++++++++++
 1 file changed, 32 insertions(+)
 create mode 100644 test/Slicing/field-sensitivity-hetero.c

diff --git a/test/Slicing/field-sensitivity-hetero.c b/test/Slicing/field-sensitivity-hetero.c
new file mode 100644
index 00000000..1c4be546
--- /dev/null
+++ b/test/Slicing/field-sensitivity-hetero.c
@@ -0,0 +1,32 @@
+// RUN: %llvmgcc %s -emit-llvm -O0 -c -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --skip-functions=foo --output-dir=%t.klee-out %t1.bc > %t2.out 2> %t2.out
+// RUN: FileCheck %s -input-file=%t2.out
+// RUN: test ! -f %t.klee-out/test000001.ptr.err
+
+// CHECK: 1 (good!)
+// CHECK: recovery states = 2
+// CHECK-NOT: (bad!)
+
+#include <stdio.h>
+
+int off = 0;
+char* file = "12";
+
+void foo(char *x) {
+   x[0] = file[off++];
+}
+
+void bar(char* x) {
+   x[0] = file[off++];
+}
+
+int main(int argc, char** argv) {
+    char a, b;
+    foo(&a);
+    bar(&b);
+
+    if (a == '1')
+      printf("1 (good!)\n");
+    else printf("%d (bad!)\n", a);
+}
\ No newline at end of file

From 88b2a38fd85b32f7ee8eb5d27951273dcaecba61 Mon Sep 17 00:00:00 2001
From: Jordy Ruiz <jruiz@ic.ac.uk>
Date: Mon, 30 Mar 2020 18:23:05 +0200
Subject: [PATCH 2/2] Add field-insensitive information upon reaching a
 field-sensitive store Possibly dealing with #42

---
 lib/Analysis/ModRefAnalysis.cpp | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/lib/Analysis/ModRefAnalysis.cpp b/lib/Analysis/ModRefAnalysis.cpp
index f85770b1..d919e471 100644
--- a/lib/Analysis/ModRefAnalysis.cpp
+++ b/lib/Analysis/ModRefAnalysis.cpp
@@ -181,6 +181,15 @@ void ModRefAnalysis::addStore(
             assert(false);
         }
 
+        // if nodeId is field-sensitive, add field-insensitive info too
+        bool insensitive = aa->getPTA()->getFIObjNode(nodeId) == nodeId;
+        if(!insensitive) {
+            NodeID FInodeId = aa->getPTA()->getFIObjNode(nodeId);
+            pair<Function *, NodeID> k = make_pair(f, FInodeId);
+            objToStoreMap[k].insert(store);
+            modPts.set(FInodeId);
+        }
+
         /* TODO: check static objects? */
         if (obj->getMemObj()->isStack()) {
             const Value *value = obj->getMemObj()->getRefVal();