immunant / c2rust

Migrate C code to Rust
https://c2rust.com/
Other
3.79k stars 219 forks source link

dataflow: avoid propagating offset permissions upward from field access #1031

Closed aneksteind closed 8 months ago

aneksteind commented 9 months ago

Pointers to structs with array fields being iterated over via offset were erroneously being given OFFSET permissions. Those permissions should be limited to the fields themselves. This PR introduces a new dataflow constraint that will propagate permissions except for a specified set. When a field projection is detected, offset permissions are no longer propagated to the base pointer.