Skip to content

Commit

Permalink
Exclude Charon when running clippy
Browse files Browse the repository at this point in the history
  • Loading branch information
zhassan-aws committed Oct 1, 2024
1 parent 6b8e692 commit fb086ea
Show file tree
Hide file tree
Showing 2 changed files with 9 additions and 10 deletions.
2 changes: 1 addition & 1 deletion .github/workflows/format-check.yml
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,7 @@ jobs:
- name: 'Run Clippy'
run: |
cargo clippy --all -- -D warnings
cargo clippy --workspace --exclude charon --exclude macros --no-deps -- -D warnings
- name: 'Print Clippy Statistics'
run: |
Expand Down
17 changes: 8 additions & 9 deletions kani-driver/src/args/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -636,16 +636,15 @@ impl ValidateArgs for VerificationArgs {
));
}

if self.common_args.unstable_features.contains(UnstableFeature::Aeneas) {
if !self.cbmc_args.is_empty() {
return Err(Error::raw(
ErrorKind::ArgumentConflict,
"The `--cbmc-args` argument cannot be used with -Z aeneas.",
));
}
// TODO: error out for other CBMC-backend-specific arguments
// TODO: error out for other CBMC-backend-specific arguments
if self.common_args.unstable_features.contains(UnstableFeature::Aeneas)
&& !self.cbmc_args.is_empty()
{
return Err(Error::raw(
ErrorKind::ArgumentConflict,
"The `--cbmc-args` argument cannot be used with -Z aeneas.",
));
}

Ok(())
}
}
Expand Down

0 comments on commit fb086ea

Please sign in to comment.