Apron: Do not produce invariants about stale locals that have escaped

src/analyses/apron/relationAnalysis.apron.ml

@@ -603,6 +603,10 @@ struct
           | Some (Local v) ->
             if VH.mem v_ins_inv v then
               keep_global
+            else if ThreadEscape.has_escaped ask v then
+              (* Escaped local variables should be read in via their v#in# variables, this apron var may refer to stale values only *)
+              (* and is not a sound description of the C variable. *)
+              false
             else
               keep_local
           | _ -> false

tests/regression/46-apron2/96-witness-mm-escape2.c

@@ -0,0 +1,22 @@
+// PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.validate 95-witness-mm-escape.yml
+#include<pthread.h>
+int *b;
+pthread_mutex_t e;
+
+void* other(void* arg) {
+    pthread_mutex_lock(&e);
+    *b = -100;
+    pthread_mutex_unlock(&e);
+
+    return NULL;
+}
+
+void main() {
+    pthread_t t;
+    pthread_create(&t, NULL, other, NULL);
+    int g = 8;
+
+    b = &g;
+
+    pthread_mutex_lock(&e);
+}

tests/regression/46-apron2/96-witness-mm-escape2.t

@@ -0,0 +1,18 @@
+  $ goblint --disable ana.dead-code.lines --disable warn.race --disable warn.behavior --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --enable witness.yaml.enabled --disable witness.invariant.other --disable witness.invariant.loop-head 96-witness-mm-escape2.c --set witness.yaml.path 96-witness-mm-escape2.yml
+  [Info][Witness] witness generation summary:
+    total generation entries: 5
+
+  $ goblint --disable ana.dead-code.lines --disable warn.race --disable warn.behavior --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.validate 96-witness-mm-escape2.yml 96-witness-mm-escape2.c
+  [Success][Witness] invariant confirmed: (unsigned long )arg == 0UL (96-witness-mm-escape2.c:8:5)
+  [Success][Witness] invariant confirmed: -128 <= g (96-witness-mm-escape2.c:22:1)
+  [Success][Witness] invariant confirmed: g <= 127 (96-witness-mm-escape2.c:22:1)
+  [Success][Witness] invariant confirmed: g != 0 (96-witness-mm-escape2.c:22:1)
+  [Info][Witness] witness validation summary:
+    confirmed: 8
+    unconfirmed: 0
+    refuted: 0
+    error: 0
+    unchecked: 0
+    unsupported: 0
+    disabled: 0
+    total validation entries: 8