Currently, if the active file is a submodule in a module directory, then we don't send Verus the full module path name, and only the name of the module itself, causing Verus to throw an error about not knowing about that module. Instead, we should be accounting for directories along the way from the root, and make sure that we pass the full path to the module.
As a quick example, consider the following directory tree:
Cargo.toml
src/
lib.rs
foo/
mod.rs
bar.rs
Then we need to send --verify-module foo::bar, and not just --verify-module bar
Currently, if the active file is a submodule in a module directory, then we don't send Verus the full module path name, and only the name of the module itself, causing Verus to throw an error about not knowing about that module. Instead, we should be accounting for directories along the way from the root, and make sure that we pass the full path to the module.
As a quick example, consider the following directory tree:
Then we need to send
--verify-module foo::bar, and not just--verify-module bar