Use same invalidation strategy as base (References #1535)

Author: michael-schwarz

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 ()))
 

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 <pthread.h>
+#include <goblint.h>
+#include <stdio.h>
+
+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;
+}