c2rust icon indicating copy to clipboard operation
c2rust copied to clipboard

analyze: Path- or context-sensitive analysis

Open ahomescu opened this issue 5 months ago • 0 comments

For the following example

fn main() {
    let x = 42;
    let mut p1 = &x as *const i32;
    let p2 = p1;
    p1 = 0 as *const i32;
}

the static analyzer assigns p1 and p2 to the same equivalence class and considers both of them nullable. The dynamic analyzer correctly marks p2 as NON_NULL, but we have no good way right now to feed that back into the static one. The unsound approach from https://github.com/immunant/c2rust/pull/1086 is extra broken, because enabling C2RUST_ANALYZE_PDG_ALLOW_UNSOUND also forces p1 to NON_NULL.

ahomescu avatar Aug 31 '24 05:08 ahomescu