[fix] Small fixes and tests

lib/Module/Locations.cpp

@@ -51,7 +51,7 @@ bool Location::isInside(const FunctionInfo &info) const {
     if (isOSSeparator(filename[n]))
       return true;
   }
-  return suffixSize >= 3 && n == -1 && m == -1;
+  return suffixSize >= 3 && (n == -1 ? (m == -1 || isOSSeparator(info.file[m])) : (m == -1 && isOSSeparator(filename[n])));
 }
 
 std::string Location::toString() const {

test/Industry/fp_forward_null_address.c

@@ -0,0 +1,27 @@
+#include <stdio.h>
+
+#define MAX_LENGTH 100
+typedef unsigned int U32;
+
+int g_arr[MAX_LENGTH];
+
+void foo()
+{
+  int *p = NULL;
+  U32 loopCntMax = MAX_LENGTH;
+  U32 i;
+  for (i = 0; i < loopCntMax; i++) {
+    if (g_arr[i] > 10) {
+      p = &g_arr[i];
+      break;
+    }
+  }
+  if (i >= loopCntMax) {
+    return;
+  }
+  int v = *p; // CHECK: KLEE: WARNING: False Positive at: /mnt/d/wsl-ubuntu/test2/forward_null/fp_forward_null_address.c:22
+}
+// RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --execution-mode=error-guided --mock-external-calls --posix-runtime --libc=klee --skip-not-lazy-and-symbolic-pointers --max-time=120s --analysis-reproduce=%s.json %t1.bc
+// RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s

test/Industry/fp_forward_null_address.c.json

@@ -0,0 +1,33 @@
+{
+    "errors": [
+        {
+            "category": "NULL pointer deference",
+            "trace": [
+                {
+                    "location": {
+                        "file": "/mnt/d/wsl-ubuntu/test2/forward_null/fp_forward_null_address.c",
+                        "reportLine": 10,
+                        "function": "foo"
+                    },
+                    "event": {
+                        "kind": "NoOp"
+                    }
+                },
+                {
+                    "location": {
+                        "file": "/mnt/d/wsl-ubuntu/test2/forward_null/fp_forward_null_address.c",
+                        "reportLine": 22,
+                        "function": "foo"
+                    },
+                    "event": {
+                        "kind": "Error",
+                        "error": {
+                            "sort": "NullDereference",
+                            "target": "p"
+                        }
+                    }
+                }
+            ]
+        }
+    ]
+}

test/Industry/fp_null_returns_self_define.c

@@ -0,0 +1,26 @@
+// RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --execution-mode=error-guided --mock-external-calls --posix-runtime --libc=klee --skip-not-lazy-and-symbolic-pointers --max-time=120s --analysis-reproduce=%s.json %t1.bc
+// RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s
+#include <stdio.h>
+
+
+unsigned int *g_status;
+unsigned int *MyValue(unsigned short index)
+{
+  if (index > 5) {
+    return NULL;                                  // (1)
+  }
+  return g_status;
+}
+
+void TEST_NullReturns004(unsigned short index)
+{
+  if (index > 5) {
+    return;
+  }
+  unsigned int *value = MyValue(index);           // (2)
+  if (*value == 0) { /* expect NULL_RETURNS */    // CHECK: KLEE: WARNING: False Positive at: /mnt/d/wsl-ubuntu/test2/null_returns/fp_null_returns_self_define.c:23
+    return;
+  }
+}

test/Industry/fp_null_returns_self_define.c.json

@@ -0,0 +1,44 @@
+{
+    "errors": [
+        {
+            "category": "NULL pointer deference",
+            "trace": [
+                {
+                    "location": {
+                        "file": "/mnt/d/wsl-ubuntu/test2/null_returns/fp_null_returns_self_define.c",
+                        "reportLine": 12,
+                        "function": "MyValue"
+                    },
+                    "event": {
+                        "kind": "NoOp"
+                    }
+                },
+                {
+                    "location": {
+                        "file": "/mnt/d/wsl-ubuntu/test2/null_returns/fp_null_returns_self_define.c",
+                        "reportLine": 22,
+                        "function": "TEST_NullReturns004"
+                    },
+                    "event": {
+                        "kind": "ExitCall",
+                        "function": "MyValue"
+                    }
+                },
+                {
+                    "location": {
+                        "file": "/mnt/d/wsl-ubuntu/test2/null_returns/fp_null_returns_self_define.c",
+                        "reportLine": 23,
+                        "function": "TEST_NullReturns004"
+                    },
+                    "event": {
+                        "kind": "Error",
+                        "error": {
+                            "sort": "NullDereference",
+                            "target": "value"
+                        }
+                    }
+                }
+            ]
+        }
+    ]
+}

test/Industry/test.c

@@ -0,0 +1,25 @@
+#include <stdio.h>
+
+char *gDest;
+
+char *HelpTestBad8(int len)
+{
+#if 0
+        if (len > 0) {
+                return gDest;
+        }
+#endif
+        return NULL;
+}
+
+void TestBad8(int len)
+{
+        // char *buf = HelpTestBad8(len);
+        char *buf = (char *)malloc(10);
+        buf[0] = 'a'; // CHECK: KLEE: WARNING: True Positive at: /mnt/d/wsl-ubuntu/test2/./test.c:19
+}
+
+// RUN: %clang %s -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -o %t1.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --execution-mode=error-guided --mock-external-calls --posix-runtime --libc=klee --skip-not-lazy-and-symbolic-pointers --check-out-of-memory --max-time=120s --analysis-reproduce=%s.json %t1.bc
+// RUN: FileCheck -input-file=%t.klee-out/warnings.txt %s

test/Industry/test.c.json

@@ -0,0 +1,33 @@
+{
+    "errors": [
+        {
+            "category": "NULL pointer deference",
+            "trace": [
+                {
+                    "location": {
+                        "file": "/mnt/d/wsl-ubuntu/test2/./test.c",
+                        "reportLine": 18,
+                        "function": "TestBad8"
+                    },
+                    "event": {
+                        "kind": "NoOp"
+                    }
+                },
+                {
+                    "location": {
+                        "file": "/mnt/d/wsl-ubuntu/test2/./test.c",
+                        "reportLine": 19,
+                        "function": "TestBad8"
+                    },
+                    "event": {
+                        "kind": "Error",
+                        "error": {
+                            "sort": "NullDereference",
+                            "target": "buf"
+                        }
+                    }
+                }
+            ]
+        }
+    ]
+}