Minor edits for all RFCs

adpaco-aws · Jun 23, 2023 · 1051a52 · 1051a52
1 parent 3224cbd
commit 1051a52
Show file tree

Hide file tree

Showing 7 changed files with 19 additions and 10 deletions.
diff --git a/rfc/src/rfcs/0001-mir-linker.md b/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

diff --git a/rfc/src/rfcs/0002-function-stubbing.md b/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.

diff --git a/rfc/src/rfcs/0003-cover-statement.md b/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
 

diff --git a/rfc/src/rfcs/0004-loop-contract-synthesis.md b/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.

diff --git a/rfc/src/rfcs/0005-should-panic-attr.md b/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.

diff --git a/rfc/src/rfcs/0006-unstable-api.md b/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
 
 -------------------

diff --git a/rfc/src/template.md b/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?