hax
hax copied to clipboard
Assuming transitive dependencies via `+~`
Say we have the following crate:
mod a {
fn need_b() {
crate::b::need_c()
}
}
mod b {
pub(super) fn need_c() {
crate::c::c()
}
}
mod c {
pub(super) fn c() {}
}
And say we want to extract all items in crate::a and their dependencies, but assume anything from crate::c. Running an extraction like
cargo hax into -i '-** +~**::a::**' pro-verif --assume-items '+**::c::'
one might think that crate::c::c would also be extracted via +~, since it's a (transitive) dependency for something in crate::a, and then assumed. At the moment, however, only crate::b::need_c is extracted and nothing from crate::c is extracted.
This can be worked around by asking instead for
cargo hax into -i '-** +~**::a::** +~**::b::need_c' pro-verif --assume-items '+**::c::'
Depending how many transitive dependencies there are it could become a bit much to manually include whatever has transitive dependencies one would like to assume.