Skip to content

Commit 5f55c49

Browse files
author
Carolyn Zech
committed
remove positive memory check options
1 parent 4ed1570 commit 5f55c49

File tree

1 file changed

+3
-46
lines changed

1 file changed

+3
-46
lines changed

kani-driver/src/args/mod.rs

Lines changed: 3 additions & 46 deletions
Original file line numberDiff line numberDiff line change
@@ -486,81 +486,39 @@ pub enum OutputFormat {
486486
#[derive(Debug, clap::Args)]
487487
#[clap(next_help_heading = "Memory Checks")]
488488
pub struct CheckArgs {
489-
// Rust argument parsers (/clap) don't have the convenient '--flag' and '--no-flag' boolean pairs, so approximate
490-
// We're put both here then create helper functions to "intepret"
491-
/// Turn on all default checks
492-
#[arg(long, hide = true)]
493-
pub default_checks: bool,
494489
/// Turn off all default checks
495490
#[arg(long)]
496491
pub no_default_checks: bool,
497492

498-
/// Turn on default memory safety checks
499-
#[arg(long, hide = true)]
500-
pub memory_safety_checks: bool,
501493
/// Turn off default memory safety checks
502494
#[arg(long)]
503495
pub no_memory_safety_checks: bool,
504496

505-
/// Turn on default overflow checks
506-
#[arg(long, hide = true)]
507-
pub overflow_checks: bool,
508497
/// Turn off default overflow checks
509498
#[arg(long)]
510499
pub no_overflow_checks: bool,
511500

512-
/// Turn on undefined function checks
513-
#[arg(long, hide = true)]
514-
pub undefined_function_checks: bool,
515501
/// Turn off undefined function checks
516502
#[arg(long)]
517503
pub no_undefined_function_checks: bool,
518504

519-
/// Turn on default unwinding checks
520-
#[arg(long, hide = true)]
521-
pub unwinding_checks: bool,
522505
/// Turn off default unwinding checks
523506
#[arg(long)]
524507
pub no_unwinding_checks: bool,
525508
}
526509

527510
impl CheckArgs {
528511
pub fn memory_safety_on(&self) -> bool {
529-
!self.no_default_checks && !self.no_memory_safety_checks || self.memory_safety_checks
512+
!self.no_default_checks && !self.no_memory_safety_checks
530513
}
531514
pub fn overflow_on(&self) -> bool {
532-
!self.no_default_checks && !self.no_overflow_checks || self.overflow_checks
515+
!self.no_default_checks && !self.no_overflow_checks
533516
}
534517
pub fn undefined_function_on(&self) -> bool {
535518
!self.no_default_checks && !self.no_undefined_function_checks
536-
|| self.undefined_function_checks
537519
}
538520
pub fn unwinding_on(&self) -> bool {
539-
!self.no_default_checks && !self.no_unwinding_checks || self.unwinding_checks
540-
}
541-
pub fn print_deprecated(&self, verbosity: &CommonArgs) {
542-
let deprecation_version = "0.63.0";
543-
let alternative = "omitting the argument, since this is already the default behavior";
544-
if self.default_checks {
545-
print_deprecated(verbosity, "--default-checks", deprecation_version, alternative);
546-
}
547-
if self.memory_safety_checks {
548-
print_deprecated(verbosity, "--memory-safety-checks", deprecation_version, alternative);
549-
}
550-
if self.overflow_checks {
551-
print_deprecated(verbosity, "--overflow-checks", deprecation_version, alternative);
552-
}
553-
if self.undefined_function_checks {
554-
print_deprecated(
555-
verbosity,
556-
"--undefined-function-checks",
557-
deprecation_version,
558-
alternative,
559-
);
560-
}
561-
if self.unwinding_checks {
562-
print_deprecated(verbosity, "--unwinding-checks", deprecation_version, alternative);
563-
}
521+
!self.no_default_checks && !self.no_unwinding_checks
564522
}
565523
}
566524

@@ -820,7 +778,6 @@ impl ValidateArgs for VerificationArgs {
820778

821779
// Check for any deprecated/obsolete options, or providing an unstable flag that has since been stabilized.
822780
let deprecated_stabilized_obsolete = || -> Result<(), Error> {
823-
self.checks.print_deprecated(&self.common_args);
824781
if self.write_json_symtab {
825782
return Err(Error::raw(
826783
ErrorKind::ValueValidation,

0 commit comments

Comments
 (0)