YAML: Relational invariants about escaped variables are incorrect (due to Apron->CIL conversion not considering escaping)

[michael-schwarz]

Consider:

#include<pthread.h>
int *b;
pthread_mutex_t e;

void* other(void* arg) {
    *b = -100;

    return NULL;
}

void main() {
    pthread_t t;
    pthread_create(&t, NULL, other, NULL);
    int g = 8;

    b = &g;

    pthread_mutex_lock(&e);
}

We produce invariants 8LL - (long long )g >= 0LL and -8LL + (long long )g >= 0LL before the lock, where the latter does not hold.
It seems that the invariants talk about stale variables corresponding to locals and no appropriate filtering is performed when turning Apron things back into assertions to avoid writing out invariants that only speak about parts of the values of variables.

The last example in #1542 could also be a result of this, only that the claimed invariant holds in the concrete by coincidence.

Commands to reproduce

`./goblint --conf conf/traces-rel.json --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --enable allglobs -v --enable witness.yaml.enabled 1.c --set witness.yaml.path 1.yml`

./goblint --conf conf/traces-rel.json --set dbg.timeout 4000 --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 1.c --enable allglobs --enable dbg.timing.enabled -v --set witness.yaml.validate ./1.yml