diff --git a/Cargo.lock b/Cargo.lock index c0ba4c91fc24..be844014995b 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -985,6 +985,7 @@ dependencies = [ "lazy_static", "num", "quote", + "regex", "serde", "serde_json", "strum", diff --git a/docs/src/reference/experimental/autoharness.md b/docs/src/reference/experimental/autoharness.md index 1fa184c484bc..95cebc9c7738 100644 --- a/docs/src/reference/experimental/autoharness.md +++ b/docs/src/reference/experimental/autoharness.md @@ -43,45 +43,37 @@ autoharness feature means that you are also opting into the function contracts a Kani generates and runs these harnesses internally—the user only sees the verification results. ### Options -The `autoharness` subcommand has options `--include-pattern` and `--exclude-pattern` to include and exclude particular functions. -These flags look for partial matches against the fully qualified name of a function. - -For example, if a module `my_module` has many functions, but we are only interested in `my_module::foo` and `my_module::bar`, we can run: -``` -cargo run autoharness -Z autoharness --include-pattern my_module::foo --include-pattern my_module::bar -``` -To exclude `my_module` entirely, run: -``` -cargo run autoharness -Z autoharness --exclude-pattern my_module -``` +The `autoharness` subcommand has options `--include-pattern [REGEX]` and `--exclude-pattern [REGEX]` to include and exclude particular functions using regular expressions. +When matching, Kani prefixes the function's path with the crate name. For example, a function `foo` in the `my_crate` crate will be matched as `my_crate::foo`. The selection algorithm is as follows: - If only `--include-pattern`s are provided, include a function if it matches any of the provided patterns. - If only `--exclude-pattern`s are provided, include a function if it does not match any of the provided patterns. - If both are provided, include a function if it matches an include pattern *and* does not match any of the exclude patterns. Note that this implies that the exclude pattern takes precedence, i.e., if a function matches both an include pattern and an exclude pattern, it will be excluded. -Here are some more examples: +Here are some examples: -``` -# Include functions whose paths contain the substring foo or baz, but not foo::bar -kani autoharness -Z autoharness --include-pattern foo --include-pattern baz --exclude-pattern foo::bar +```bash +# Include functions containing foo but not bar +kani autoharness -Z autoharness --include-pattern 'foo' --exclude-pattern 'bar' + +# Include my_crate::foo exactly +kani autoharness -Z autoharness --include-pattern '^my_crate::foo$' -# Include functions whose paths contain the substring foo, but not bar. -kani autoharness -Z autoharness --include-pattern foo --exclude-pattern bar +# Include functions in the foo module, but not in foo::bar +kani autoharness -Z autoharness --include-pattern 'foo::.*' --exclude-pattern 'foo::bar::.*' -# Include functions whose paths contain the substring foo::bar, but not bar. -# This ends up including nothing, since all foo::bar matches will also contain bar. -# Kani will emit a warning that these flags conflict. -kani autoharness -Z autoharness --include-pattern foo::bar --exclude-pattern bar +# Include functions starting with test_, but not if they're in a private module +kani autoharness -Z autoharness --include-pattern 'test_.*' --exclude-pattern '.*::private::.*' -# Include functions whose paths contain the substring foo, but not foo. -# This ends up including nothing, and Kani will emit a warning that these flags conflict. -kani autoharness -Z autoharness --include-pattern foo --exclude--pattern foo +# This ends up including nothing since all foo::bar matches will also contain bar. +# Kani will emit a warning that these options conflict. +kani autoharness -Z autoharness --include-pattern 'foo::bar' --exclude-pattern 'bar' ``` -Currently, the only supported "patterns" are substrings of the fully qualified path of the function. -However, if more sophisticated patterns (e.g., regular expressions) would be useful for you, -please let us know in a comment on [this GitHub issue](https://github.com/model-checking/kani/issues/3832). +Note that because Kani prefixes function paths with the crate name, some patterns might match more than you expect. +For example, given a function `foo_top_level` inside crate `my_crate`, the regex `.*::foo_.*` will match `foo_top_level`, since Kani interprets it as `my_crate::foo_top_level`. +To match only `foo_` functions inside modules, use a more specific pattern, e.g. `.*::[^:]+::foo_.*`. ## Example Using the `estimate_size` example from [First Steps](../../tutorial-first-steps.md) again: diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index afe4cb3241cb..b4193cec36d7 100644 --- a/kani-compiler/Cargo.toml +++ b/kani-compiler/Cargo.toml @@ -17,6 +17,7 @@ kani_metadata = { path = "../kani_metadata" } lazy_static = "1.5.0" num = { version = "0.4.0", optional = true } quote = "1.0.36" +regex = "1.11.1" serde = { version = "1", optional = true } serde_json = "1" strum = "0.27.1" diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs index 336c45ab55d6..9715d9976b61 100644 --- a/kani-compiler/src/kani_middle/codegen_units.rs +++ b/kani-compiler/src/kani_middle/codegen_units.rs @@ -21,6 +21,7 @@ use kani_metadata::{ ArtifactType, AssignsContract, AutoHarnessMetadata, AutoHarnessSkipReason, HarnessKind, HarnessMetadata, KaniMetadata, }; +use regex::RegexSet; use rustc_hir::def_id::DefId; use rustc_middle::ty::TyCtxt; use rustc_session::config::OutputType; @@ -356,6 +357,29 @@ fn get_all_automatic_harnesses( .collect::>() } +fn make_regex_set(patterns: Vec) -> Option { + if patterns.is_empty() { + None + } else { + Some(RegexSet::new(patterns).unwrap_or_else(|e| { + panic!("Invalid regexes should have been caught during argument validation: {e}") + })) + } +} + +/// A function is filtered out if 1) none of the include patterns match it or 2) one of the exclude patterns matches it. +fn autoharness_filtered_out( + name: &str, + included_set: &Option, + excluded_set: &Option, +) -> bool { + // A function is included if `--include-pattern` is not provided or if at least one of its regexes matches `name` + let included = included_set.as_ref().is_none_or(|set| set.is_match(name)); + // A function is excluded if `--exclude-pattern` is provided and at least one of its regexes matches `name` + let excluded = excluded_set.as_ref().is_some_and(|set| set.is_match(name)); + !included || excluded +} + /// Partition every function in the crate into (chosen, skipped), where `chosen` is a vector of the Instances for which we'll generate automatic harnesses, /// and `skipped` is a map of function names to the reason why we skipped them. fn automatic_harness_partition( @@ -364,12 +388,15 @@ fn automatic_harness_partition( crate_name: &str, kani_any_def: FnDef, ) -> (Vec, BTreeMap) { - // If `filter_list` contains `name`, either as an exact match or a substring. - let filter_contains = |name: &str, filter_list: &[String]| -> bool { - filter_list.iter().any(|filter_name| name.contains(filter_name)) - }; + let crate_fns = + stable_mir::all_local_items().into_iter().filter(|item| item.ty().kind().is_fn()); + + let included_set = make_regex_set(args.autoharness_included_patterns.clone()); + let excluded_set = make_regex_set(args.autoharness_excluded_patterns.clone()); // If `func` is not eligible for an automatic harness, return the reason why; if it is eligible, return None. + // Note that we only return one reason for ineligiblity, when there could be multiple; + // we can revisit this implementation choice in the future if users request more verbose output. let skip_reason = |fn_item: CrateItem| -> Option { if KaniAttributes::for_def_id(tcx, fn_item.def_id()).is_kani_instrumentation() { return Some(AutoHarnessSkipReason::KaniImpl); @@ -397,34 +424,8 @@ fn automatic_harness_partition( return Some(AutoHarnessSkipReason::KaniImpl); } - match ( - args.autoharness_included_patterns.is_empty(), - args.autoharness_excluded_patterns.is_empty(), - ) { - // If no filters were specified, then continue. - (true, true) => {} - // If only --exclude-pattern was provided, filter out the function if excluded_patterns contains its name. - (true, false) => { - if filter_contains(&name, &args.autoharness_excluded_patterns) { - return Some(AutoHarnessSkipReason::UserFilter); - } - } - // If only --include-pattern was provided, filter out the function if included_patterns does not contain its name. - (false, true) => { - if !filter_contains(&name, &args.autoharness_included_patterns) { - return Some(AutoHarnessSkipReason::UserFilter); - } - } - // If both are specified, filter out the function if included_patterns does not contain its name. - // Then, filter out any functions that excluded_patterns does match. - // This order is important, since it preserves the semantics described in kani_driver::autoharness_args where exclude takes precedence over include. - (false, false) => { - if !filter_contains(&name, &args.autoharness_included_patterns) - || filter_contains(&name, &args.autoharness_excluded_patterns) - { - return Some(AutoHarnessSkipReason::UserFilter); - } - } + if autoharness_filtered_out(&name, &included_set, &excluded_set) { + return Some(AutoHarnessSkipReason::UserFilter); } // Each argument of `instance` must implement Arbitrary. @@ -472,14 +473,6 @@ fn automatic_harness_partition( let mut chosen = vec![]; let mut skipped = BTreeMap::new(); - // FIXME: ideally, this filter would be matches!(item.kind(), ItemKind::Fn), since that would allow us to generate harnesses for top-level closures, - // c.f. https://github.com/model-checking/kani/issues/3832#issuecomment-2701671798. - // Note that filtering closures out here is a UX choice: we could instead call skip_reason() on closures, - // but the limitations in the linked issue would cause the user to be flooded with reports of "skipping" Kani instrumentation functions. - // Instead, we just pretend closures don't exist in our reporting of what we did and did not verify, which has the downside of also ignoring the user's top-level closures, but those are rare. - let crate_fns = - stable_mir::all_local_items().into_iter().filter(|item| item.ty().kind().is_fn()); - for func in crate_fns { if let Some(reason) = skip_reason(func) { skipped.insert(func.name(), reason); @@ -490,3 +483,179 @@ fn automatic_harness_partition( (chosen, skipped) } + +#[cfg(test)] +mod autoharness_filter_tests { + use super::*; + + #[test] + fn both_none() { + let included = None; + let excluded = None; + assert!(!autoharness_filtered_out("test_fn", &included, &excluded)); + } + + #[test] + fn only_included() { + let included = make_regex_set(vec!["test.*".to_string()]); + let excluded = None; + + assert!(!autoharness_filtered_out("test_fn", &included, &excluded)); + assert!(autoharness_filtered_out("other_fn", &included, &excluded)); + } + + #[test] + fn only_excluded() { + let included = None; + let excluded = make_regex_set(vec!["test.*".to_string()]); + + assert!(autoharness_filtered_out("test_fn", &included, &excluded)); + assert!(!autoharness_filtered_out("other_fn", &included, &excluded)); + } + + #[test] + fn both_matching() { + let included = make_regex_set(vec![".*_fn".to_string()]); + let excluded = make_regex_set(vec!["test.*".to_string()]); + + assert!(autoharness_filtered_out("test_fn", &included, &excluded)); + assert!(!autoharness_filtered_out("other_fn", &included, &excluded)); + } + + #[test] + fn multiple_include_patterns() { + let included = make_regex_set(vec!["test.*".to_string(), "other.*".to_string()]); + let excluded = None; + + assert!(!autoharness_filtered_out("test_fn", &included, &excluded)); + assert!(!autoharness_filtered_out("other_fn", &included, &excluded)); + assert!(autoharness_filtered_out("different_fn", &included, &excluded)); + } + + #[test] + fn multiple_exclude_patterns() { + let included = None; + let excluded = make_regex_set(vec!["test.*".to_string(), "other.*".to_string()]); + + assert!(autoharness_filtered_out("test_fn", &included, &excluded)); + assert!(autoharness_filtered_out("other_fn", &included, &excluded)); + assert!(!autoharness_filtered_out("different_fn", &included, &excluded)); + } + + #[test] + fn exclude_precedence_identical_patterns() { + let pattern = "test.*".to_string(); + let included = make_regex_set(vec![pattern.clone()]); + let excluded = make_regex_set(vec![pattern]); + + assert!(autoharness_filtered_out("test_fn", &included, &excluded)); + assert!(autoharness_filtered_out("other_fn", &included, &excluded)); + } + + #[test] + fn exclude_precedence_overlapping_patterns() { + let included = make_regex_set(vec![".*_fn".to_string()]); + let excluded = make_regex_set(vec!["test_.*".to_string(), "other_.*".to_string()]); + + assert!(autoharness_filtered_out("test_fn", &included, &excluded)); + assert!(autoharness_filtered_out("other_fn", &included, &excluded)); + assert!(!autoharness_filtered_out("different_fn", &included, &excluded)); + } + + #[test] + fn exact_match() { + let included = make_regex_set(vec!["^test_fn$".to_string()]); + let excluded = None; + + assert!(!autoharness_filtered_out("test_fn", &included, &excluded)); + assert!(autoharness_filtered_out("test_fn_extra", &included, &excluded)); + } + + #[test] + fn include_specific_module() { + let included = make_regex_set(vec!["module1::.*".to_string()]); + let excluded = None; + + assert!(!autoharness_filtered_out("module1::test_fn", &included, &excluded)); + assert!(!autoharness_filtered_out("crate::module1::test_fn", &included, &excluded)); + assert!(autoharness_filtered_out("module2::test_fn", &included, &excluded)); + assert!(autoharness_filtered_out("crate::module2::test_fn", &included, &excluded)); + } + + #[test] + fn exclude_specific_module() { + let included = None; + let excluded = make_regex_set(vec![".*::internal::.*".to_string()]); + + assert!(autoharness_filtered_out("crate::internal::helper_fn", &included, &excluded)); + assert!(autoharness_filtered_out("my_crate::internal::test_fn", &included, &excluded)); + assert!(!autoharness_filtered_out("crate::public::test_fn", &included, &excluded)); + } + + #[test] + fn test_exact_match_with_crate() { + let included = make_regex_set(vec!["^lib::foo_function$".to_string()]); + let excluded = None; + + assert!(!autoharness_filtered_out("lib::foo_function", &included, &excluded)); + assert!(autoharness_filtered_out("lib::foo_function_extra", &included, &excluded)); + assert!(autoharness_filtered_out("lib::other::foo_function", &included, &excluded)); + assert!(autoharness_filtered_out("other::foo_function", &included, &excluded)); + assert!(autoharness_filtered_out("foo_function", &included, &excluded)); + } + + #[test] + fn complex_path_patterns() { + let included = make_regex_set(vec![ + "crate::module1::.*".to_string(), + "other_crate::tests::.*".to_string(), + ]); + let excluded = + make_regex_set(vec![".*::internal::.*".to_string(), ".*::private::.*".to_string()]); + + assert!(!autoharness_filtered_out("crate::module1::test_fn", &included, &excluded)); + assert!(!autoharness_filtered_out("other_crate::tests::test_fn", &included, &excluded)); + assert!(autoharness_filtered_out( + "crate::module1::internal::test_fn", + &included, + &excluded + )); + assert!(autoharness_filtered_out( + "other_crate::tests::private::test_fn", + &included, + &excluded + )); + assert!(autoharness_filtered_out("crate::module2::test_fn", &included, &excluded)); + } + + #[test] + fn crate_specific_filtering() { + let included = make_regex_set(vec!["my_crate::.*".to_string()]); + let excluded = make_regex_set(vec!["other_crate::.*".to_string()]); + + assert!(!autoharness_filtered_out("my_crate::test_fn", &included, &excluded)); + assert!(!autoharness_filtered_out("my_crate::module::test_fn", &included, &excluded)); + assert!(autoharness_filtered_out("other_crate::test_fn", &included, &excluded)); + assert!(autoharness_filtered_out("third_crate::test_fn", &included, &excluded)); + } + + #[test] + fn root_crate_paths() { + let included = make_regex_set(vec!["^crate::.*".to_string()]); + let excluded = None; + + assert!(!autoharness_filtered_out("crate::test_fn", &included, &excluded)); + assert!(autoharness_filtered_out("other_crate::test_fn", &included, &excluded)); + assert!(autoharness_filtered_out("test_fn", &included, &excluded)); + } + + #[test] + fn impl_paths_with_spaces() { + let included = make_regex_set(vec!["num::::wrapping_.*".to_string()]); + let excluded = None; + + assert!(!autoharness_filtered_out("num::::wrapping_sh", &included, &excluded)); + assert!(!autoharness_filtered_out("num::::wrapping_add", &included, &excluded)); + assert!(autoharness_filtered_out("num::::wrapping_sh", &included, &excluded)); + } +} diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml index be47ae1b5e5c..afd9acff9c65 100644 --- a/kani-driver/Cargo.toml +++ b/kani-driver/Cargo.toml @@ -22,7 +22,7 @@ serde = { version = "1", features = ["derive"] } serde_json = { version = "1", features = ["preserve_order"] } clap = { version = "4.4.11", features = ["derive"] } toml = "0.8" -regex = "1.6" +regex = "1.11.1" rustc-demangle = "0.1.21" pathdiff = "0.2.1" rayon = "1.5.3" diff --git a/kani-driver/src/args/autoharness_args.rs b/kani-driver/src/args/autoharness_args.rs index 6d329627bd13..93d9eb439127 100644 --- a/kani-driver/src/args/autoharness_args.rs +++ b/kani-driver/src/args/autoharness_args.rs @@ -6,28 +6,20 @@ use std::path::PathBuf; use crate::args::list_args::Format; use crate::args::{ValidateArgs, VerificationArgs, validate_std_path}; +use crate::util::warning; use clap::{Error, Parser, error::ErrorKind}; use kani_metadata::UnstableFeature; +use regex::Regex; -// TODO: It would be nice if we could borrow --exact here from VerificationArgs to differentiate between partial/exact matches, -// like --harnesses does. Sharing arguments with VerificationArgs doesn't work with our current structure, though. #[derive(Debug, Parser)] pub struct CommonAutoharnessArgs { - /// Only create automatic harnesses for functions that match the given pattern. - /// This option can be provided multiple times, which will verify functions matching any of the patterns. - /// Kani considers a function to match the pattern if its fully qualified path contains PATTERN as a substring. - /// Example: `--include-pattern foo` matches all functions whose fully qualified paths contain the substring "foo". + /// Only create automatic harnesses for functions that match the given regular expression. #[arg(long = "include-pattern", num_args(1), value_name = "PATTERN")] pub include_pattern: Vec, - /// Only create automatic harnesses for functions that do not match the given pattern. - /// This option can be provided multiple times, which will verify functions that do not match any of the patterns. - /// Kani considers a function to match the pattern if its fully qualified path contains PATTERN as a substring. - + /// Only create automatic harnesses for functions that do not match the given regular expression pattern. /// This option takes precedence over `--include-pattern`, i.e., Kani will first select all functions that match `--include-pattern`, /// then exclude those that match `--exclude-pattern.` - /// Example: `--include-pattern foo --exclude-pattern foo::bar` creates automatic harnesses for all functions whose paths contain "foo" without "foo::bar". - /// Example: `--include-pattern foo::bar --exclude-pattern foo` makes the `--include-pattern` a no-op, since the exclude pattern is a superset of the include pattern. #[arg(long = "exclude-pattern", num_args(1), value_name = "PATTERN")] pub exclude_pattern: Vec, @@ -72,8 +64,47 @@ pub struct StandaloneAutoharnessArgs { pub verify_opts: VerificationArgs, } +impl ValidateArgs for CommonAutoharnessArgs { + fn validate(&self) -> Result<(), Error> { + // Error gracefully if a pattern contains whitespace, since rustc_driver argument will panic later if we try to pass this back, + // c.f. https://github.com/model-checking/kani/issues/4046 + for pattern in self.include_pattern.iter().chain(self.exclude_pattern.iter()) { + if pattern.contains(char::is_whitespace) { + return Err(Error::raw( + ErrorKind::InvalidValue, + "The `--include-pattern` and `--exclude-pattern` options do not support patterns with whitespace. \ + Use regular expression pattern flags (e.g., . to match any character) instead.", + )); + } + if let Err(e) = Regex::new(pattern) { + return Err(Error::raw( + ErrorKind::InvalidValue, + format!("invalid autoharness regular expression pattern: {e}"), + )); + } + } + + for include_pattern in self.include_pattern.iter() { + for exclude_pattern in self.exclude_pattern.iter() { + // Check if include pattern contains exclude pattern + // This catches cases like include="foo::bar" exclude="bar" or include="foo" exclude="foo" + if include_pattern.contains(exclude_pattern) { + warning(&format!( + "Include pattern '{include_pattern}' contains exclude pattern '{exclude_pattern}'. \ + This combination will never match any functions since all functions matching \ + the include pattern will also match the exclude pattern, and the exclude pattern takes precedence." + )); + } + } + } + + Ok(()) + } +} + impl ValidateArgs for CargoAutoharnessArgs { fn validate(&self) -> Result<(), Error> { + self.common_autoharness_args.validate()?; self.verify_opts.validate()?; if !self.verify_opts.common_args.unstable_features.contains(UnstableFeature::Autoharness) { return Err(Error::raw( @@ -113,6 +144,7 @@ impl ValidateArgs for CargoAutoharnessArgs { impl ValidateArgs for StandaloneAutoharnessArgs { fn validate(&self) -> Result<(), Error> { + self.common_autoharness_args.validate()?; self.verify_opts.validate()?; if !self.verify_opts.common_args.unstable_features.contains(UnstableFeature::Autoharness) { return Err(Error::raw( diff --git a/kani-driver/src/autoharness/mod.rs b/kani-driver/src/autoharness/mod.rs index f4bcd221ec08..01904bb786d6 100644 --- a/kani-driver/src/autoharness/mod.rs +++ b/kani-driver/src/autoharness/mod.rs @@ -14,7 +14,6 @@ use crate::list::collect_metadata::process_metadata; use crate::list::output::output_list_results; use crate::project::{Project, standalone_project, std_project}; use crate::session::KaniSession; -use crate::util::warning; use crate::{InvocationType, print_kani_version, project, verify_project}; use anyhow::Result; use comfy_table::Table as PrettyTable; @@ -163,20 +162,6 @@ impl KaniSession { /// Add the compiler arguments specific to the `autoharness` subcommand. pub fn add_auto_harness_args(&mut self, included: &[String], excluded: &[String]) { - for include_pattern in included { - for exclude_pattern in excluded { - // Check if include pattern contains exclude pattern - // This catches cases like include="foo::bar" exclude="bar" or include="foo" exclude="foo" - if include_pattern.contains(exclude_pattern) { - warning(&format!( - "Include pattern '{include_pattern}' contains exclude pattern '{exclude_pattern}'. \ - This combination will never match any functions since all functions matching \ - the include pattern will also match the exclude pattern, and the exclude pattern takes precedence." - )); - } - } - } - let mut args = vec![]; for pattern in included { args.push(format!("--autoharness-include-pattern {pattern}")); diff --git a/tests/script-based-pre/kani_autoharness_exclude_precedence/precedence.sh b/tests/script-based-pre/kani_autoharness_exclude_precedence/precedence.sh index 38b92b88c740..7879625e824c 100755 --- a/tests/script-based-pre/kani_autoharness_exclude_precedence/precedence.sh +++ b/tests/script-based-pre/kani_autoharness_exclude_precedence/precedence.sh @@ -64,13 +64,13 @@ verify_functions() { local exclude_pattern="$3" for func in "${FUNCTIONS[@]}"; do - # If the function name matches the include pattern and not the exclude pattern, it should be selected - if echo "$func" | grep -q "$include_pattern" && ! echo "$func" | grep -q "$exclude_pattern"; then + local full_path="lib::$func" + + if [[ -z "$include_pattern" || "$full_path" =~ $include_pattern ]] && [[ -z "$exclude_pattern" || ! "$full_path" =~ $exclude_pattern ]]; then if ! check_selected "$output" "$func"; then echo "ERROR: Expected $func to be selected" exit 1 fi - # Otherwise, it should be skipped else if ! check_skipped "$output" "$func"; then echo "ERROR: Expected $func to be skipped" @@ -80,12 +80,18 @@ verify_functions() { done } -# Test cases test_cases=( "include 'foo' exclude 'foo::bar'" "include 'foo' exclude 'bar'" "include 'foo::bar' exclude 'bar'" "include 'foo' exclude 'foo'" + "include 'foo::.*' exclude 'foo::bar::.*'" + "include 'foo::.*' exclude '.*bar.*'" + "include 'foo::bar::.*' exclude '.*bar_function$'" + "include '^foo.*' exclude '^foo.*'" + "include '.*::foo_.*' exclude '.*::bar::.*'" + "include '^[^:]+$' exclude '.*_top_level$'" + "include '.*' exclude '^foo::.*'" ) include_patterns=( @@ -93,6 +99,13 @@ include_patterns=( "foo" "foo::bar" "foo" + "foo::.*" + "foo::.*" + "foo::bar::.*" + "^foo.*" + ".*::foo_.*" + "^[^:]+$" + ".*" ) exclude_patterns=( @@ -100,6 +113,13 @@ exclude_patterns=( "bar" "bar" "foo" + "foo::bar::.*" + ".*bar.*" + ".*bar_function$" + "^foo.*" + ".*::bar::.*" + ".*_top_level$" + "^foo::.*" ) # Whether each test case should produce a warning about no functions being selected @@ -108,6 +128,13 @@ should_warn=( false true true + false + false + false + true + false + false + false ) for i in "${!test_cases[@]}"; do diff --git a/tests/script-based-pre/kani_autoharness_exclude_precedence/src/lib.rs b/tests/script-based-pre/kani_autoharness_exclude_precedence/src/lib.rs index 8fb3d7957ae3..6e14b154f802 100644 --- a/tests/script-based-pre/kani_autoharness_exclude_precedence/src/lib.rs +++ b/tests/script-based-pre/kani_autoharness_exclude_precedence/src/lib.rs @@ -1,6 +1,8 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT +#![allow(dead_code)] + mod foo { fn foo_function() {}