From 993a0455cbdde81e5eaa41d3a1890f09ac9258b6 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 2 Nov 2023 12:25:38 +0200 Subject: [PATCH 1/4] Extract both branches dead test from concrat/Remotery --- tests/regression/00-sanity/41-both_branches-2.c | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) create mode 100644 tests/regression/00-sanity/41-both_branches-2.c 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; +} From 4ea07567add44655631166371103c1512a32b678 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 2 Nov 2023 12:37:03 +0200 Subject: [PATCH 2/4] Fix both branches dead from bot address in array Fix from https://github.com/goblint/analyzer/issues/1188#issuecomment-1735060169. --- src/cdomains/valueDomain.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/cdomains/valueDomain.ml b/src/cdomains/valueDomain.ml index cba4b04c18..003a65a49e 100644 --- a/src/cdomains/valueDomain.ml +++ b/src/cdomains/valueDomain.ml @@ -201,7 +201,7 @@ struct 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 (if can_recover_from_top then (top_value ai) else Bot)) | TNamed ({ttype=t; _}, _) -> top_value ~varAttr t | _ -> Top From 2d1b4204574733c7f081a1c5f2b859b22da04eeb Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 10 Jan 2024 12:06:51 +0200 Subject: [PATCH 3/4] Use only tops for arrays in ValueDomain.top_value --- src/cdomains/valueDomain.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/cdomains/valueDomain.ml b/src/cdomains/valueDomain.ml index 003a65a49e..8fb639deb9 100644 --- a/src/cdomains/valueDomain.ml +++ b/src/cdomains/valueDomain.ml @@ -199,9 +199,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)) + Array (CArrays.make ~varAttr ~typAttr len (top_value ai)) | TNamed ({ttype=t; _}, _) -> top_value ~varAttr t | _ -> Top From 11e89489ee3ffe7b9587d64a6e0d9994cb55cc9f Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 10 Jan 2024 12:09:13 +0200 Subject: [PATCH 4/4] Mark fixed TODOs in 03-practical/31-zstd-cctxpool-blobs --- tests/regression/03-practical/31-zstd-cctxpool-blobs.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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; }