hax icon indicating copy to clipboard operation
hax copied to clipboard

Assuming transitive dependencies via `+~`

Open jschneider-bensch opened this issue 1 year ago • 0 comments

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.

jschneider-bensch avatar Feb 29 '24 09:02 jschneider-bensch