Stabilize cover statement and update contracts RFC

library/kani/src/mem.rs

@@ -44,7 +44,7 @@ use std::ptr::{DynMetadata, NonNull, Pointee};
 /// Note that an unaligned pointer is still considered valid.
 ///
 /// TODO: Kani should automatically add those checks when a de-reference happens.
-/// https://github.com/model-checking/kani/issues/2975
+/// <https://github.com/model-checking/kani/issues/2975>
 ///
 /// This function will either panic or return `true`. This is to make it easier to use it in
 /// contracts.

rfc/src/rfcs/0003-cover-statement.md

@@ -1,8 +1,8 @@
 - **Feature Name:** Cover statement (`cover-statement`)
 - **Feature Request Issue:** <https://github.com/model-checking/kani/issues/696>
 - **RFC PR:** <https://github.com/model-checking/kani/pull/1906>
-- **Status:** Unstable
-- **Version:** 1
+- **Status:** Stable
+- **Version:** 2
 
 -------------------
 
@@ -138,8 +138,12 @@ However, if the condition can indeed be covered, verification would fail due to
 
 ## Open questions
 
-Should we allow format arguments in the macro, e.g. `kani::cover!(x > y, "{} can be greater than {}", x, y)`?
-Users may expect this to be supported since the macro looks similar to the `assert` macro, but Kani doesn't include the formatted string in the message description, since it's not available at compile time.
+- ~Should we allow format arguments in the macro, e.g. `kani::cover!(x > y, "{} can be greater than {}", x, y)`?
+Users may expect this to be supported since the macro looks similar to the `assert` macro, but Kani doesn't include the formatted string in the message description, since it's not available at compile time.~
+  - For now, this macro will not accept format arguments, since this
+    is not well handled by Kani.
+    This is an extesion to this API that can be easily added later on if Kani
+    ever supports runtime formatting.
 
 ## Other Considerations
 

rfc/src/rfcs/0009-function-contracts.md

@@ -1,8 +1,8 @@
 - **Feature Name:** Function Contracts
 - **Feature Request Issue:** [#2652](https://github.com/model-checking/kani/issues/2652) and [Milestone](https://github.com/model-checking/kani/milestone/31)
 - **RFC PR:** [#2620](https://github.com/model-checking/kani/pull/2620)
-- **Status:** Under Review 
-- **Version:** 0
+- **Status:** Unstable
+- **Version:** 1
 - **Proof-of-concept:** [features/contracts](https://github.com/model-checking/kani/tree/features/contracts)
 - **Feature Gate:** `-Zfunction-contracts`, enforced by compile time error[^gate]
 
@@ -893,4 +893,5 @@ times larger than what they expect the function will touch).
 
 [^stubcheck]: Kani cannot report the occurrence of a contract function to check
     in abstracted functions as errors, because the mechanism is needed to verify
-    mutually recursive functions.
+    mutually recursive functions.
+

scripts/build-docs.sh

@@ -28,8 +28,10 @@ else
       curl -sSL -o "$FILE" "$URL"
       echo "$EXPECTED_HASH $FILE" | sha256sum -c -
       tar zxf $FILE
+      MDBOOK=${SCRIPT_DIR}/mdbook
+  else
+      MDBOOK=mdbook
   fi
-  MDBOOK=${SCRIPT_DIR}/mdbook
 fi
 
 KANI_DIR=$SCRIPT_DIR/..