CIL pulls up all declarations inside a function to the top-level scope of that function. This transformation turns code that has Undefined Behavior into code without any UB, which is of course perfectly ok for a compiler to do, but bad for tools who want to flag this type of UB despite working on the output of CIL.

An example of this is the following snippet:

int* ptr;

for(int i =0; i <20; i++) {
    int j =8;
    
    if(i ==0) {
        ptr = &j;
    }
    
    // Will work with most (all) compilers without a hitch, but technically is UB,
    // as ptr points to an object whose lifetime has ended in all but the first iteration 
    *ptr = 5;
}

After CIL, j is pulled to the top scope and there is no more UB.

A rewrite to properly handle scopes seems tedious, and also of questionable value, since it would be a breaking change and would make using CIL more complicated.

This adds an option addNestedScopeAttr to cabs2cil. When it is enabled, this adds an attribute goblint_cil_nested to all varinfos for locals that occur inside a nested scope. This way, sound tools can overapproximate for which variables there may be issues.

As the flag is off by default, this should not cause any changes in behavior for other users.

c.f. goblint/analyzer#1199