diff --git a/src/cdomain/value/cdomains/valueDomain.ml b/src/cdomain/value/cdomains/valueDomain.ml index d1b81dcb08..d748706ad1 100644 --- a/src/cdomain/value/cdomains/valueDomain.ml +++ b/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 diff --git a/tests/regression/00-sanity/41-both_branches-2.c b/tests/regression/00-sanity/41-both_branches-2.c new file mode 100644 index 0000000000..4bfd339b13 --- /dev/null +++ b/tests/regression/00-sanity/41-both_branches-2.c @@ -0,0 +1,17 @@ +// PARAM: --disable sem.unknown_function.invalidate.globals +#include +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; +} diff --git a/tests/regression/03-practical/31-zstd-cctxpool-blobs.c b/tests/regression/03-practical/31-zstd-cctxpool-blobs.c index 40e448eb22..c91c141446 100644 --- a/tests/regression/03-practical/31-zstd-cctxpool-blobs.c +++ b/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; }