Suggestions from @feliperodri

cprover_bindings/src/goto_program/symbol_table.rs

@@ -80,6 +80,8 @@ impl SymbolTable {
  self.symbol_table.get_mut(&name).unwrap().update_fn_declaration_with_definition(body);
  }
 
+ /// Attach a contract to the symbol identified by `name`. If a prior
+ /// contract exists it is extended with additional clauses.
  pub fn attach_contract<T: Into<InternedString>>(
  &mut self,
  name: T,

library/kani_macros/src/lib.rs

@@ -167,14 +167,30 @@ pub fn stub_verified(attr: TokenStream, item: TokenStream) -> TokenStream {
  attr_impl::stub_verified(attr, item)
 }
 
+/// Declaration of an explicit write-set for the annotated function.
+///
+/// This is part of the function contract API, for more general information see
+/// the [module-level documentation](../kani/contracts/index.html).
+///
+/// The contents of the attribute is a series of comma-separated expressions referencing the
+/// arguments of the function. Each expression is expected to return a pointer type, i.e. `*const T`,
+/// `*mut T`, `&T` or `&mut T`. The pointed-to type must implement
+/// [`Arbitrary`](../kani/arbitrary/trait.Arbitrary.html).
+///
+/// All Rust syntax is supported, even calling other functions, but the computations must be side
+/// effect free, e.g. it cannot perform I/O or use mutable memory.
+///
+/// Kani requires each function that uses a contract to have at least one designated
+/// [`proof_for_contract`][macro@proof_for_contract] harness for checking the
+/// contract.
 #[proc_macro_attribute]
 pub fn modifies(attr: TokenStream, item: TokenStream) -> TokenStream {
  attr_impl::modifies(attr, item)
 }
 
 /// This module implements Kani attributes in a way that only Kani's compiler can understand.
 /// This code should only be activated when pre-building Kani's sysroot.
-#[cfg(kani_sysroot)]
+//#[cfg(kani_sysroot)]
 mod sysroot {
  use proc_macro_error::{abort, abort_call_site};
 

library/kani_macros/src/sysroot/contracts.rs

@@ -1319,11 +1319,12 @@ fn hash_of_token_stream<H: std::hash::Hasher>(hasher: &mut H, stream: proc_macro
 /// Hash this `TokenStream` and return an integer that is at most digits
 /// long when hex formatted.
 fn short_hash_of_token_stream(stream: &proc_macro::TokenStream) -> u64 {
+ const SIX_HEX_DIGITS_MASK: u64 = 0x1_000_000;
  use std::hash::Hasher;
  let mut hasher = std::collections::hash_map::DefaultHasher::default();
  hash_of_token_stream(&mut hasher, proc_macro2::TokenStream::from(stream.clone()));
  let long_hash = hasher.finish();
- long_hash % 0x1_000_000 // six hex digits
+ long_hash % SIX_HEX_DIGITS_MASK
 }
 
 /// Makes consistent names for a generated function which was created for

tests/expected/function-contract/.unsafe_assigns_rc

@@ -30,4 +30,4 @@ fn main() {
 // let i = Rc::new(RefCell::new(begin));
 // modify(i.clone());
 // kani::assert(*i.borrow() == begin + 1, "end");
-// }
+// }