From 508d7e2ca658541859e1a867a87579a8c31fb5d7 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sat, 6 Jul 2024 17:02:44 +0200 Subject: [PATCH] Use same invalidation strategy as base (References #1535) --- src/analyses/apron/relationAnalysis.apron.ml | 7 +++---- tests/regression/46-apron2/98-invalidate.c | 22 ++++++++++++++++++++ 2 files changed, 25 insertions(+), 4 deletions(-) create mode 100644 tests/regression/46-apron2/98-invalidate.c diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index df3cf545c5..f2ea577527 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/src/analyses/apron/relationAnalysis.apron.ml @@ -469,10 +469,9 @@ struct | None -> None | Some st -> let ad = ask.f (Queries.ReachableFrom e) in - if Queries.AD.is_top ad then - None - else - Some (Queries.AD.join ad st) + (* See https://github.com/goblint/analyzer/issues/1535 *) + let ad = Queries.AD.remove UnknownPtr ad in + Some (Queries.AD.join ad st) in List.fold_right reachable es (Some (Queries.AD.empty ())) diff --git a/tests/regression/46-apron2/98-invalidate.c b/tests/regression/46-apron2/98-invalidate.c new file mode 100644 index 0000000000..948b70e3ce --- /dev/null +++ b/tests/regression/46-apron2/98-invalidate.c @@ -0,0 +1,22 @@ +// SKIP PARAM: --set ana.activated[+] apron --set sem.int.signed_overflow assume_none +#include +#include +#include + +int debug; +int other; + +int main() { + int top; + + // Needed so Base & DefExc doesn't find this information because it invalidates less + if(top) { + debug = 3; + } + + fscanf(stdin, "%d", &other); + + // Fails as debug is invalidated + __goblint_check(debug <= 3); + return 0; +}