Allow --verify-function more than once

source/rust_verify/src/config.rs

@@ -94,7 +94,7 @@ pub struct ArgsX {
     pub verify_root: bool,
     pub verify_module: Vec<String>,
     pub verify_only_module: Vec<String>,
-    pub verify_function: Option<String>,
+    pub verify_function: Vec<String>,
     pub no_external_by_default: bool,
     pub no_verify: bool,
     pub no_lifetime: bool,
@@ -573,11 +573,11 @@ pub fn parse_args_with_imports(
         "Verify just one submodule (excluding its descendants) within the crate (e.g. 'foo' or 'foo::bar'), can be repeated to verify only certain modules",
         "MODULE",
     );
-    opts.optopt(
+    opts.optmulti(
         "",
         OPT_VERIFY_FUNCTION,
-        "Verify just one function within the one module specified by verify-module or verify-root, \nmatches on unique substring (foo) or wildcards at ends of the argument (*foo, foo*, *foo*)",
-        "MODULE",
+        "Verify just the functions matched by this pattern, within the modules given by verify-only-module and verify-root, \nmatches on unique substring (foo) or wildcards at ends of the argument (*foo, foo*, *foo*), \ncan be repeated to verify the union of the functions matched by each pattern; \na pattern with :: is also matched against each function's path from the crate root (foo::bar::f or crate::foo::bar::f, or crate::f for the root) \nand against its module's path followed by its name relative to the module (foo::S::f for a method of an impl of S in module foo); \na pattern without * at its ends is matched against names relative to the module first, then against these paths; \nif it matches functions in more than one module, it is an error",
+        "PATTERN",
     );
     opts.optflag("", OPT_NO_EXTERNAL_BY_DEFAULT, "(deprecated) Verify all items, even those declared outside the verus! macro, and even if they aren't marked #[verifier::verify]");
     opts.optflag("", OPT_NO_VERIFY, "Do not run verification");
@@ -835,14 +835,8 @@ pub fn parse_args_with_imports(
                             .to_owned(),
                     )
                 }
-                if matches.opt_count(OPT_VERIFY_ONLY_MODULE)
-                    + (if matches.opt_present(OPT_VERIFY_ROOT) { 1 } else { 0 })
-                    > 1
-                {
-                    error("Must pass at most one --verify-only-module or --verify-root when using --verify-function".to_string())
-                }
             }
-            matches.opt_str(OPT_VERIFY_FUNCTION)
+            matches.opt_strs(OPT_VERIFY_FUNCTION)
         },
         no_external_by_default: matches.opt_present(OPT_NO_EXTERNAL_BY_DEFAULT),
         no_verify: matches.opt_present(OPT_NO_VERIFY),

source/rust_verify/src/driver.rs

@@ -33,7 +33,7 @@ fn run_compiler<'a, 'b>(
 }
 
 pub fn is_verifying_entire_crate(verifier: &Verifier) -> bool {
-    verifier.args.verify_function.is_none()
+    verifier.args.verify_function.is_empty()
         && verifier.args.verify_module.is_empty()
         && !verifier.args.verify_root
 }