Allow pointer arithmethic on UnknownPtr to give NullPtr as well

Author: sim642

src/analyses/base.ml

@@ -312,7 +312,12 @@ struct
           | `Top -> AD.top_ptr
         end
       | UnknownPtr
-      | StrPtr _ -> AD.unknown_ptr
+      | StrPtr _ ->
+        begin match ID.equal_to Z.zero n with
+          | `Eq -> AD.singleton addr (* remains unchanged *)
+          | `Neq
+          | `Top -> AD.top_ptr
+        end
     in
     let ad_concat_map f a = AD.fold (fun a acc -> AD.join (f a) acc) a (AD.empty ()) in
     let addToAddrOp p (n:ID.t):value =

tests/regression/01-cpa/79-null-ptr-arith.c

@@ -3,4 +3,18 @@ int main(void) {
   int i;
   int *q = p + i;
   *q = 42; // WARN (may NULL dereference)
+
+  if (p) {
+    q = p + i;
+    *q = 42; // WARN (may NULL dereference)
+
+    if (i == 0) {
+      q = p + i;
+      *q = 42; // NOWARN (no NULL dereference)
+    }
+    else {
+      q = p + i;
+      *q = 42; // WARN (may NULL dereference)
+    }
+  }
 }