Merge pull request #602 from goblint/issue-566

Fix imprecise AD.meet with NULL

src/cdomains/addressDomain.ml

@@ -125,7 +125,7 @@ struct
       else remove Addr.NullPtr x
     in
     match is_top x, is_top y with
-    | true, true -> uop x y
+    | true, true -> no_null (no_null (uop x y) x) y
     | false, true -> no_null x y
     | true, false -> no_null y x
     | false, false -> cop x y

tests/regression/27-inv_invariants/15-unknown-null-ptr.c

@@ -6,10 +6,10 @@ int main() {
   if (r == NULL)
     assert(r == NULL);
   else
-    assert(r != NULL); // TODO
+    assert(r != NULL);
 
   if (r != NULL)
-    assert(r != NULL); // TODO
+    assert(r != NULL);
   else
     assert(r == NULL);
 

tests/regression/27-inv_invariants/16-sedgewick.c

@@ -0,0 +1,26 @@
+#include <stddef.h>
+#include <assert.h>
+
+struct node {
+  struct node *left;
+  struct node *right;
+  int key;
+};
+
+// https://old.reddit.com/r/programminghorror/comments/jgrpcu/on_sedgewicks_original_presentation_for_llrb_trees/
+struct node* min(struct node *root) {
+  struct node *x = root;
+  while (x != NULL)
+    x = x->left;
+  if (x == NULL) // WARN (dead branch)
+    return NULL;
+  else
+    return x;
+}
+
+int main() {
+  struct node *root;
+  struct node *m = min(root);
+  assert(m == NULL);
+  return 0;
+}