diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml index dd4b65bab8..61da6ddc42 100644 --- a/src/analyses/apron/relationPriv.apron.ml +++ b/src/analyses/apron/relationPriv.apron.ml @@ -813,7 +813,9 @@ struct let g_var = V.global g in (* normal (strong) mapping: contains only still fully protected *) let g' = VS.singleton g in - let oct = LRD.find g' octs in + (* If there is no map entry yet which contains the global, default to top rather than bot *) + (* Happens e.g. in 46/86 because of escape *) + let oct = Option.default (RD.top ()) (LRD.find_opt g' octs) in LRD.singleton g' (RD.keep_vars oct [g_var]) let lock_get_m oct local_m get_m = diff --git a/tests/regression/46-apron2/86-escape-cluster12.c b/tests/regression/46-apron2/86-escape-cluster12.c new file mode 100644 index 0000000000..283e45b728 --- /dev/null +++ b/tests/regression/46-apron2/86-escape-cluster12.c @@ -0,0 +1,21 @@ +// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 +#include +#include +void *a; + +void* nothing(void* arg) { + // Go multithreaded! +} + +void main() { + pthread_t t; + pthread_create(&t, 0, nothing, 0); + + int d = 5; + a = &d; + + if (0) + ; + + __goblint_check(1); // Should be reachable! +}