Users should be able to use RMC to target functions with the same name in different modules. For example, if user wants to verify the following code:

mod first {
    fn check() {
        // some check
    }
}

mod second {
    fn check() {
        // check for second module
    }
}

pub fn check() {
  // full check
}

They should be able to provide which function they want to check. I.e:

rmc multiple.rs --function [check | first::check | second::check]

Note that users cannot use #[no_mangle] for the check functions, since this would cause a name conflict. The compilation would fail with the following error:

error: symbol `check` is already defined
  --> multiple.rs:26:1
   |
26 | fn check() {
   | ^^^^^^^^^^^^^^

error: aborting due to previous error