From f01b619716b044659bbce2193476bcaf1a937ec0 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Thu, 14 Dec 2023 13:55:34 -0500 Subject: [PATCH] Apply suggestions from code review Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs | 4 ++-- library/kani/src/contracts.rs | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index f38fff0df7d5..944a8586e73c 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -201,11 +201,11 @@ impl<'tcx> GotocCtx<'tcx> { /// for which it needs to be enforced. /// /// 1. Gets the `#[kanitool::inner_check = "..."]` target, then resolves exactly one instance - /// of it. Panics there are more or less than one instance. + /// of it. Panics if there are more or less than one instance. /// 2. Expects that a `#[kanitool::modifies(...)]` is placed on the `inner_check` function, /// turns it into a CBMC contract and attaches it to the symbol for the previously resolved /// instance. - /// 3. Returns the mangled of the symbol it attached the contract to. + /// 3. Returns the mangled name of the symbol it attached the contract to. /// 4. Resolves the `#[kanitool::checked_with = "..."]` target from `function_under_contract` /// which has `static mut REENTRY : bool` declared inside. /// 5. Returns the full path to this constant that `--nondet-static-exclude` expects which is diff --git a/library/kani/src/contracts.rs b/library/kani/src/contracts.rs index 90fda5ac90b5..07e1b4cfaa19 100644 --- a/library/kani/src/contracts.rs +++ b/library/kani/src/contracts.rs @@ -127,7 +127,7 @@ //! `result`. //! //! In addition Kani provides the [`modifies`](macro@modifies) attribute. This -//! works a bit different int aht it does not contain conditions but a comma +//! works a bit different in that it does not contain conditions but a comma //! separated sequence of expressions that evaluate to pointers. This attribute //! constrains to which memory locations the function is allowed to write. Each //! expression can contain arbitrary Rust syntax, though it may not perform side @@ -203,7 +203,7 @@ //! The [`modifies`](macro@modifies) attribute is used to describe which //! locations in memory a function may assign to. The attribute contains a comma //! separated series of expressions that reference the function arguments. -//! Syntactically any expression id permissible, though it may not perform side +//! Syntactically any expression is permissible, though it may not perform side //! effects (I/O, mutation) or panic. As an example consider this super simple //! function: //!