Merge branch 'main' into kk-exec-viz

kani-dependencies

@@ -1,4 +1,4 @@
-CBMC_VERSION="5.85.0"
+CBMC_VERSION="5.86.0"
 # If you update this version number, remember to bump it in `src/setup.rs` too
 CBMC_VIEWER_VERSION="3.8"
 KISSAT_VERSION="3.0.0"

rfc/src/rfcs/0001-mir-linker.md

@@ -1,4 +1,4 @@
-- **Feature Name:** MIR Linker (mir_linker)
+- **Feature Name:** MIR Linker (`mir_linker`)
 - **RFC Tracking Issue**: <https://github.com/model-checking/kani/issues/1588>
 - **RFC PR:** <https://github.com/model-checking/kani/pull/1600>
 - **Status:** Stable

rfc/src/rfcs/0002-function-stubbing.md

@@ -1,10 +1,12 @@
-- **Feature Name:** Function and method stubbing (`function_stubbing`)
+- **Feature Name:** Function and method stubbing (`function-stubbing`)
 - **Feature Request Issue:** <https://github.com/model-checking/kani/issues/1695>
 - **RFC PR:** <https://github.com/model-checking/kani/pull/1723> 
-- **Status:** Under Review
+- **Status:** Unstable
 - **Version:** 1
 - **Proof-of-concept:** <https://github.com/aaronbembenek-aws/kani/tree/mir_transform>
 
+-------------------
+
 ## Summary
 
 Allow users to specify that certain functions and methods should be replaced with mock functions (stubs) during verification.

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

@@ -1,9 +1,10 @@
-- **Feature Name:** Cover statement `cover_statement`
+- **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:** Under Review
+- **Status:** Unstable
 - **Version:** 0
-- **Proof-of-concept:** *Optional field. If you have implemented a proof of concept, add a link here*
+
+-------------------
 
 ## Summary
 

rfc/src/rfcs/0004-loop-contract-synthesis.md

@@ -1,10 +1,12 @@
-- **Feature Name:** Loop-contract synthesis
+- **Feature Name:** Loop-contract synthesis (`loop-contract-synthesis`)
 - **Feature Request Issue:** <https://github.com/model-checking/kani/issues/2214>
 - **RFC PR:** <https://github.com/model-checking/kani/pull/2215>
 - **Status:** Under Review
 - **Version:** 0
 - **Proof-of-concept:** <https://github.com/qinheping/kani/tree/kani-synthesizer>
 
+-------------------
+
 ## Summary
 
 A new option that allows users to verify programs without unwinding loops by synthesizing loop contracts for those loops.

rfc/src/rfcs/0005-should-panic-attr.md

@@ -1,10 +1,12 @@
-- **Feature Name:** The `kani::should_panic` attribute (`should-panic-attr`)*
+- **Feature Name:** The `kani::should_panic` attribute (`should-panic-attr`)
 - **Feature Request Issue:** <https://github.com/model-checking/kani/issues/600>
 - **RFC PR:** <https://github.com/model-checking/kani/pull/2272>
-- **Status:** Under Review
+- **Status:** Unstable
 - **Version:** 0
 - **Proof-of-concept:** <https://github.com/model-checking/kani/pull/2315>
 
+-------------------
+
 ## Summary
 
 Users may want to express that a verification harness should panic.

rfc/src/rfcs/0006-unstable-api.md

@@ -1,7 +1,7 @@
 - **Feature Name:** Unstable APIs (`unstable-api`)
 - **RFC Tracking Issue**: <https://github.com/model-checking/kani/issues/2279>
 - **RFC PR:** <https://github.com/model-checking/kani/pull/2281>
-- **Status:** Under Review
+- **Status:** Unstable
 - **Version:** 0
 
 -------------------

rfc/src/template.md

@@ -6,6 +6,8 @@
  Start with 0.*
 - **Proof-of-concept:** *Optional field. If you have implemented a proof of concept, add a link here*
 
+-------------------
+
 ## Summary
 
 Short description of the feature, i.e.: the elevator pitch. What is this feature about?

scripts/kani-regression.sh

@@ -19,7 +19,7 @@ KANI_DIR=$SCRIPT_DIR/..
 export KANI_FAIL_ON_UNEXPECTED_DESCRIPTION="true"
 
 # Required dependencies
-check-cbmc-version.py --major 5 --minor 85
+check-cbmc-version.py --major 5 --minor 86
 check-cbmc-viewer-version.py --major 3 --minor 8
 check_kissat_version.sh