diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 13f0eddfab99..6b22b246718a 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -239,7 +239,7 @@ impl CodegenBackend for GotocCodegenBackend { // Any changes to queries from this point on is just related to caching information // needed for generating code to the given crate. - // The cached information mut not outlive the stable-mir `run` scope. + // The cached information must not outlive the stable-mir `run` scope. // See [QueryDb::kani_functions] for more information. let queries = self.queries.lock().unwrap().clone(); diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs index 0bdd4a1603b8..911ccf17e55f 100644 --- a/kani-compiler/src/kani_middle/transform/body.rs +++ b/kani-compiler/src/kani_middle/transform/body.rs @@ -436,7 +436,7 @@ impl MutableBody { } } -// TODO: Remove-me +// TODO: Remove this enum, since we now only support kani's assert. #[derive(Clone, Debug)] pub enum CheckType { /// This is used by default when the `kani` crate is available.