Skip to content

Commit

Permalink
Apply suggestions from code review
Browse files Browse the repository at this point in the history
Co-authored-by: Carolyn Zech <cmzech@amazon.com>
  • Loading branch information
celinval and carolynzech authored Nov 15, 2024
1 parent 7d45dd9 commit 6f60d4f
Show file tree
Hide file tree
Showing 3 changed files with 8 additions and 8 deletions.
4 changes: 2 additions & 2 deletions kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down
10 changes: 5 additions & 5 deletions kani-compiler/src/kani_middle/kani_functions.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -148,8 +148,8 @@ impl TryFrom<FnDef> for KaniFunction {

fn try_from(def: FnDef) -> Result<Self, Self::Error> {
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) {
Expand All @@ -165,8 +165,8 @@ impl TryFrom<Instance> for KaniFunction {

fn try_from(instance: Instance) -> Result<Self, Self::Error> {
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) {
Expand Down
2 changes: 1 addition & 1 deletion kani-compiler/src/kani_middle/transform/kani_intrinsics.rs
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,7 @@ pub struct IntrinsicGeneratorPass {
check_type: CheckType,
/// Used to cache FnDef lookups for models and Kani intrinsics.
kani_defs: HashMap<KaniFunction, FnDef>,
/// Used to enable intrinsics depending on the flags passed.
/// Whether the user enabled uninitialized memory checks when they invoked Kani.
enable_uninit: bool,
}

Expand Down

0 comments on commit 6f60d4f

Please sign in to comment.