Skip to content

Commit

Permalink
Apply suggestions from code review
Browse files Browse the repository at this point in the history
Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
  • Loading branch information
JustusAdam and zhassan-aws authored Dec 14, 2023
1 parent 34e3a1b commit f01b619
Show file tree
Hide file tree
Showing 2 changed files with 4 additions and 4 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 @@ -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
Expand Down
4 changes: 2 additions & 2 deletions library/kani/src/contracts.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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:
//!
Expand Down

0 comments on commit f01b619

Please sign in to comment.