Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

analyze: Path- or context-sensitive analysis #1118

Open
ahomescu opened this issue Aug 31, 2024 · 0 comments
Open

analyze: Path- or context-sensitive analysis #1118

ahomescu opened this issue Aug 31, 2024 · 0 comments
Labels
bug Something isn't working c2rust-analyze enhancement New feature or request

Comments

@ahomescu
Copy link
Contributor

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 #1086 is extra broken, because enabling C2RUST_ANALYZE_PDG_ALLOW_UNSOUND also forces p1 to NON_NULL.

@ahomescu ahomescu added bug Something isn't working enhancement New feature or request c2rust-analyze labels Aug 31, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working c2rust-analyze enhancement New feature or request
Projects
None yet
Development

No branches or pull requests

1 participant