Merge pull request #1233 from goblint/concrat-both-branches

Fix both branches dead from bot address in array

Author: sim642

src/cdomain/value/cdomains/valueDomain.ml

@@ -204,9 +204,8 @@ struct
     | TComp ({cstruct=false; _},_) -> Union (Unions.top ())
     | TArray (ai, length, _) ->
       let typAttr = typeAttrs ai in
-      let can_recover_from_top = ArrayDomain.can_recover_from_top (ArrayDomain.get_domain ~varAttr ~typAttr) in
       let len = array_length_idx (IndexDomain.top ()) length in
-      Array (CArrays.make ~varAttr ~typAttr len (if can_recover_from_top then (top_value ai) else (bot_value ai)))
+      Array (CArrays.make ~varAttr ~typAttr len (top_value ai))
     | TNamed ({ttype=t; _}, _) -> top_value ~varAttr t
     | _ -> Top
 

tests/regression/00-sanity/41-both_branches-2.c

@@ -0,0 +1,17 @@
+// PARAM: --disable sem.unknown_function.invalidate.globals
+#include <goblint.h>
+struct S {
+  int *f[1];
+};
+
+int main() {
+  struct S* s;
+  s = magic();
+
+  int *p = s->f[0];
+  if (p)
+    __goblint_check(1); // reachable
+  else
+    __goblint_check(1); // reachable
+  return 0;
+}

tests/regression/03-practical/31-zstd-cctxpool-blobs.c

@@ -22,8 +22,8 @@ int main() {
   ZSTDMT_CCtxPool* const cctxPool = calloc(1, sizeof(ZSTDMT_CCtxPool));
   cctxPool->cctx[0] = malloc(sizeof(ZSTD_CCtx));
   if (!cctxPool->cctx[0]) // TODO NOWARN
-    __goblint_check(1); // TODO reachable
+    __goblint_check(1); // reachable
   else
-    __goblint_check(1); // TODO reachable
+    __goblint_check(1); // reachable
   return 0;
 }