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; +}