diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index d959f327e748..16391216cd8b 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -237,8 +237,8 @@ impl CodegenBackend for GotocCodegenBackend { let ret_val = rustc_internal::run(tcx, || { super::utils::init(); - // Any changes to queries from this point on is just related to caching information - // for efficiency purpose that should not outlive the stable-mir `run` scope. + // Any changes to queries from this point on is just related to caching; + // the cached information will not outlive the stable-mir `run` scope. let queries = self.queries.lock().unwrap().clone(); check_target(tcx.sess); diff --git a/kani-compiler/src/kani_middle/kani_functions.rs b/kani-compiler/src/kani_middle/kani_functions.rs index 23d127368ef6..56098b76f36e 100644 --- a/kani-compiler/src/kani_middle/kani_functions.rs +++ b/kani-compiler/src/kani_middle/kani_functions.rs @@ -4,7 +4,7 @@ //! //! There are three types of functions today: //! 1. Kani intrinsics: These are functions whose body is generated during -//! compilation time. Their body usually require some extra knowledge about the given types +//! compilation time. Their body usually requires some extra knowledge about the given types //! that's only available during compilation. //! 2. Kani models: These are functions that model a specific behavior but that cannot be used //! directly by the user. For example, retrieving information about memory initialization. @@ -148,8 +148,8 @@ impl TryFrom for KaniFunction { fn try_from(def: FnDef) -> Result { let value = attributes::fn_marker(def).ok_or(())?; - if let Ok(intrisic) = KaniIntrinsic::from_str(&value) { - Ok(intrisic.into()) + if let Ok(intrinsic) = KaniIntrinsic::from_str(&value) { + Ok(intrinsic.into()) } else if let Ok(model) = KaniModel::from_str(&value) { Ok(model.into()) } else if let Ok(hook) = KaniHook::from_str(&value) { @@ -165,8 +165,8 @@ impl TryFrom for KaniFunction { fn try_from(instance: Instance) -> Result { let value = attributes::fn_marker(instance.def).ok_or(())?; - if let Ok(intrisic) = KaniIntrinsic::from_str(&value) { - Ok(intrisic.into()) + if let Ok(intrinsic) = KaniIntrinsic::from_str(&value) { + Ok(intrinsic.into()) } else if let Ok(model) = KaniModel::from_str(&value) { Ok(model.into()) } else if let Ok(hook) = KaniHook::from_str(&value) { diff --git a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs index 533c27445b84..9c541d1e1ee4 100644 --- a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs +++ b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs @@ -39,7 +39,7 @@ pub struct IntrinsicGeneratorPass { check_type: CheckType, /// Used to cache FnDef lookups for models and Kani intrinsics. kani_defs: HashMap, - /// Used to enable intrinsics depending on the flags passed. + /// Whether the user enabled uninitialized memory checks when they invoked Kani. enable_uninit: bool, }