Pass Escaped Locals to Callee as They Need to Be Considered Globals

[michael-schwarz]

Currently, escaped locals (pointer was saved into globals) are not correctly passed to callees, as enter filters via Basetype.Variables.is_global k instead of is_global (Analyses.ask_of_ctx ctx) k.

Looking up the corresponding value in the local state then leads to bot, which is ignored when merging over all possible addresses that a pointer may point to.

Minimal example:

#include <assert.h>
int* ptr;
int nine = 9;

int other() {
    assert(*ptr == 8); //UNKNOWN!
}

int main()
{
    int g = 8;
    int top;

    if(top) {
        ptr = &g;
    } else {
        ptr = &nine;
    }

    other();
}

TODO: Investigate if this fixes the unsoundnesses for SV-Comp.

[sim642]

Good catch! I had forgotten that the escaping into globals applies to singlethreaded mode as well. Although the module name is still ThreadEscape and its top comment also just mentions escaping to threads. Maybe we should bring that up to date.