Merge remote-tracking branch 'origin/new-assigns-check' into new-assi…

…gns-check

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

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:
 //!