VeriFast solution for Challenge 5 (linked_list.rs)

doc/src/challenges/0005-linked-list.md

@@ -1,10 +1,11 @@
 # Challenge 5: Verify functions iterating over inductive data type: `linked_list`
 
-- **Status:** Open
+- **Status:** Resolved
 - **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29)
 - **Start date:** *2024/07/01*
-- **End date:** *2025/04/10*
+- **End date:** *2025/08/12*
 - **Reward:** *5,000 USD*
+- **Contributors:** [Bart Jacobs](https://github.com/btj)
 
 -------------------
 

verifast-proofs/alloc/collections/linked_list.rs/original/lib.rs

@@ -1,4 +1,4 @@
-// verifast_options{skip_specless_fns}
+// verifast_options{skip_specless_fns ignore_unwind_paths}
 
 #![no_std]
 #![allow(internal_features)]
@@ -12,6 +12,7 @@
 #![feature(exact_size_is_empty)]
 #![feature(hasher_prefixfree_extras)]
 #![feature(box_into_inner)]
+#![feature(try_trait_v2)]
 
 #![stable(feature = "rust1", since = "1.0.0")]
 

verifast-proofs/alloc/collections/linked_list.rs/verified/lib.rs

@@ -1,4 +1,4 @@
-// verifast_options{skip_specless_fns}
+// verifast_options{skip_specless_fns ignore_unwind_paths}
 
 #![no_std]
 #![allow(internal_features)]
@@ -12,6 +12,7 @@
 #![feature(exact_size_is_empty)]
 #![feature(hasher_prefixfree_extras)]
 #![feature(box_into_inner)]
+#![feature(try_trait_v2)]
 
 #![stable(feature = "rust1", since = "1.0.0")]